An Integrated Development Environment for Formal Specifications.
Michael R. Laux, R.H. Bourdeau, Betty H. C. Cheng · 1993
As software is increasingly used to control critical systems, program correctness becomes paramount. A small change in the implementation of software can have a large and perhaps disastrous impact on its behavior. Formal methods focus a software development effort on an accurate and precise specification of what a software system or component is to achieve. This type of specification, when expressed in a precise mathematical notation, is referred to as a formal specification. Using formal specification languages facilitates the early evaluation of a software design and verification of its implementation through the use of formal reasoning techniques. Larch uses a two-tiered approach to formal specifications. One tier, the Larch Shared Language (LSL), is common to all programming languages. This paper describes a development environment that facilitates the construction of LSL specifications, including a graphical interface to theorem proving and syntax checking tools.