Executing
Formal Specifications by Translation to Higher Order Logic Programming.
by James H. Andrews
| |
Executing
Formal Specifications by Translation to Higher Order Logic Programming.
by James H. Andrews
|
| formalWARE
project
formalWARE
formalWARE
|
Abstract
We describe the construction and use of a system for translating higher order logic-based specifications into programs in the higher order logic programming language Lambda Prolog. The translation improves on previous work in the field of executing specifications by allowing formulas with quantifiers to be executed, and by permitting users to pose Prolog-style queries with free variables to be instantiated by the system. We also discuss various alternative target languages and design decisions in implementing the translator. Download Postscript
Presented at the 1997 International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, 19-22 August 1997.
|
