Unintrusive ways to integrate formal specifications in practice
journal contributionposted on 01.04.2007 by Jeannette Marie. Wing, Amy Moormann. Zaremski
Any type of content formally published in an academic journal, usually following a peer-review process.
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 Miro╠ü visual languages [HMT90]. The companion technical report, CMU-CS-91-111, contains the entire specification."