Towards Integrating Algebraic Specification and Functional Programming: the Opal System

摘要

We envisage a software engineering environment based on formal methods, that, encompasses requirements capture and formal specification as well as efficient implementation in a functional style. The overall principles to be used in such an environment have been studied, for example, in the KorSo project [2] and in the Kids project [8], in the tradition of projects such as ClP [1] and OBJ [6]. The Opal project focusses on the design and implementation of a functional language that fits into the above context. Ideally, the project, should comprise concepts for functional programming and algebraic specification, a methodology and a proof calculus for verification and synthesis and a suite of elaborate support tools. In this extended abstract we sketch the current state of the system.