Equational Programming (A Study in Executable Algebraic Formal Specification)

摘要

This report summarizes progress on the Equational Programming project sponsored by the office of Naval Research, during the period July 1, 1982 to December 31, 1985. Most of our effort during this period was devoted to designing and beginning to implement the OBJ2 equational programming language. This Language was designed and implemented in accord with the rigorous standards of logic and mathematics; were believe this to be the essence of logic programming. Moreover, a rigorous semantics leads to considerable savings in implementation effort, and need not restrict expressive power. Thus, the work on implementing OBJ2 has been closely coupled with work on its semantics, and the implementation has made essential use of various conceptual advances. The overall conception of OBJ2, with its new ideas on inheritance, views, and parameterization, was sketched by Goguen. A semantic integration of Horn clause (logic) and equational (functional) programming was done by Goguen and Messeguer in this design an semantics for the Eqlog language; containing OBJ2 as its functional sublanguage. Inheritance based upon subsorts is fundamental to both OBJ2 and Eqlog and has involved advances in both mathematical and operational semantics.