ISLET: a program/proof editor to support the Vienna Development Method

ENCOMPASS is an environment that addresses the software quality problem using a combination of executable specifications, peer review, testing, and formal techniques similar to the Vienna Development Method. One of the most important tools in ENCOMPASS is ISLET, a language-oriented program/proof editor that supports the construction of formal specifications and their incremental refinement into verified implementations. In ISLET, the refinement process can be viewed as the development of a program or as the construction of a proof of correctness. From the proof view, some refinements generate verification conditions that must be true for the step to be correct. ISLET incorporates a number of simple methods that can inexpensively certify a large percentage of the verification conditions generated. An overview of ENCOMPASS and ISLET is given, and an example of development using the editor is presented