Weitere Kapitel dieses Buchs durch Wischen aufrufen
Z is a formal specification language based on Zermelo set theory. It was developed at the Programming Research Group at Oxford University in the early 1980s and became an ISO standard in 2002. Z specifications are mathematical and employ a classical two-valued logic. The use of mathematics ensures precision, and allows inconsistencies and gaps in the specification to be identified. Theorem provers may be employed to demonstrate the correctness of the refinement steps, and that the software implementation meets its specification.
Z is a ‘model oriented’ approach with an explicit model of the state of an abstract machine given, and operations are defined in terms of this state. Its mathematical notation is used for formal specification, and the schema calculus is used to structure the specifications. The latter is visually striking, and consists essentially of boxes, with these boxes or schemas used to describe operations and states. The schema calculus enables schemas to be used as building blocks and combined with other schemas.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Step-wise refinement involves producing a sequence of increasingly more concrete specifications until eventually the executable code is produced. Each refinement step has associated proof obligations to prove that the refinement step is valid.
This project claimed a 9 % increase in productivity attributed to the use of formal methods.
Zurück zum Zitat Diller A (1990) Z. An introduction to formal methods. Wiley, England Diller A (1990) Z. An introduction to formal methods. Wiley, England
Zurück zum Zitat O’Regan G (2013) Mathematics in computing. Springer, London O’Regan G (2013) Mathematics in computing. Springer, London
- Z Formal Specification Language
ec4u, Neuer Inhalt/© ITandMEDIA