Although formal methods have the potential to greatly enhance software development, they have not been widely used in industry (particularly in the United States). We have developed a system for executing specifications by compiling them to Oz programs. Executability is a great aid in developing specifications, and also increases the usefulness of specifications by allowing them to serve as prototypes and test oracles. In this work, we describe how we have used the Oz language both as a translation target and in implementing a library of procedures used by the generated programs. Oz is ideal for our purposes, as it has allowed us to easily use declarative, concurrent constraint and graphical user interface programming together within a single framework.
展开▼
