Unintrusive ways to integrate formal specifications in practice

Abstract: "Formal methods can be neatly woven in with less formal, but more widely-used, industrial-strength methods. We show how to integrate the Larch two-tiered specification method [GHW85a] with two used in the waterfall model of software development: Structured Analysis [Ros77] and Structure Charts [YC79]. We use Larch traits to define data elements in a data dictionary and the functionality of basic activities in Structured Analysis data-flow diagrams; Larch interfaces and traits to define the behavior of modules in Structure Charts. We also show how to integrate loosely formal specification in a prototyping model by discussing ways of refining Larch specifications as code evolves.To provide some realism to our ideas, we draw our examples from a non-trivial Larch specification of the graphical editor for the Miró visual languages [HMT90]. The companion technical report, CMU-CS-91-111, contains the entire specification."