The paper briefly explains the Gypsy verification environment--an experimental system devoted to exploring the practicality of formal, mathematical approaches to software engineering. The environment provides an integrated collection of conventional software development tools, along with special tools for constructing formal proofs about the behavior of Gypsy software systems. The user interacts with the executive component of the environment in order to use a number of different software tools to build and evolve a software library. This library contains the various Gypsy components of the specification and implementation of a software system, as well as other supporting information such as verification conditions and proofs.

The Gypsy software system is developed in a top-down manner, starting from a top level external specification of its behavior. This specification consists of a mandatory environment specification describing all of the external data objects that are accessible to the procedure, and an optional operational specification describing what effect is to be caused on the objects of the external environment. The external specification is step-wise refined and the user is assisted in checking the refinement correctness by a verification condition generator, an algebraic simplifier, an interactive proof checker, and an optimizer.

The environment has been tested on a number of trial applications. The paper summarizes two major ones: a message flow modulator and a network interface. Various measures of the scale of the trial applications, and estimations of the amounts of resources are also considered. In the author’s opinion, the results have been very encouraging.

The paper is of interest for software engineers in dealing with new technologies that can provide improvements in the predictability and quality of software systems.