Formal Specification

Book Chapter

Author(s):Andreas Roth and Peter H. Schmitt
In:Verification of Object-Oriented Software: The KeY Approach
Publisher:Springer
Series:LNCS 4334
Part:II: Expressing and Formalising Requirements
Chapter:5
Year:2007
Pages:245-294
DOI:10.1007/978-3-540-69061-0_5

Abstract

This chapter serves as an introduction to formal specifications. In Sect. 5.1 we reconsider in greater detail, but still on a fairly general level, the basic building blocks of formal specification—pre- and postconditions, invariants, and modifies clauses—that have already been informally introduced in Sect. 1.3. The next two sections then show how these notions can be formulated in two popular specification languages, OCL and JML. A short comparison between the two languages in Section 5.4 concludes this chapter.

BibTeX

@incollection{RothSchmitt2007,
   author        = {Andreas Roth and Peter H. Schmitt},
   title         = {Formal Specification},
   chapter       = {5},
   part          = {II: Expressing and Formalising Requirements},
   pages         = {245--294},
   editor        = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   booktitle     = {Verification of Object-Oriented Software: The {\KeY} Approach},
   year          = {2007},
   series        = {LNCS 4334},
   publisher     = {Springer},
   doi           = {10.1007/978-3-540-69061-0_5},
   abstract      = {This chapter serves as an introduction to formal specifications.
                    In Sect. 5.1 we reconsider in greater detail, but still on a
                    fairly general level, the basic building blocks of formal
                    specification---pre- and postconditions, invariants, and
                    modifies clauses---that have already been informally introduced
                    in Sect. 1.3. The next two sections then show how these notions
                    can be formulated in two popular specification languages, OCL
                    and JML. A short comparison between the two languages in
                    Section 5.4 concludes this chapter.}
}