The extends ENCOMPASS ?79,82,85-87! a prototype environment to support the incremental construction of Ada programs using executable specifications and formal techniques similar to the Vienna Development Method. In ENCOMPASS, software is specified using PLEASE ?80,81,83,84! an executable specification language which builds on logic-programming and database technology. In ENCOMPASS, PLEASE specifications are incrementally refined into Ada implementations; refinements can be verified using testing, peer review or proof-based techniques. PLEASE supports the rigorous development of software: parts of a system can be developed using completely formal methods, while other, less critical parts are constructed using less expensive techniques. Systems can be constructed using all the features of Ada, although at present not all Ada constructs can be formally analyzed. The next phase of this research will extend the formal description of both PLEASE and the development process based on it; study the efficiency and scalability of the technologies used to implement PLEASE and ENCOMPASS; investigate the use of PLEASE in the development of large and parallel programs; and extend ENCOMPASS with more sophisticated, knowledge-based tools.
