@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.}
}
Formal Specification
| Autor(en): | Andreas Roth und Peter H. Schmitt |
|---|---|
| In: | Verification of Object-Oriented Software: The KeY Approach |
| Verleger: | Springer |
| Reihe: | LNCS 4334 |
| Teil: | II: Expressing and Formalising Requirements |
| Kapitel: | 5 |
| Jahr: | 2007 |
| Seiten: | 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.