EARLY REPORT ON ENCOMPASS.

ENCOMPASS is an environment designed to support the incremental construction of Ada programs using executable specifications and formal techniques similar to the Vienna Development Method. ENCOMPASS supports the rigorous development of software: parts of a project may use completely formal methods, while other, less critical parts use less expensive techniques. ENCOMPASS provides automated support for all aspects of the development process including specification, prototyping, testing, formal verification, documentation, configuration control, and project management. In ENCOMPASS, software can be specified using PLEASE, an Ada-based executable specification language which can be automatically translated into Prolog. A prototype implementation of ENCOMPASS has been constructed. The authors give an overview of ENCOMPASS, describe the decisions made in the design of the prototype, and discuss the lessions learned in the process.