Contents
Chapter 1 Introduction
1.1 Important note for version 2.30
Chapter 2 Tutorial
2.1 The basics of the methodology
2.2 Loop invariants
2.3 Array accesses
2.4 Logic predicates
2.5 Array updates
2.6 Objects and constructors
2.7 Calling subprograms,
assigns
clauses
2.8 Programs with exceptions
2.9 The Dutch National Flag problem
2.10 Ghost variables
Chapter 3 Specification Language: Reference
3.1 Logic expressions
3.1.1 Operator precedence
3.1.2 Semantics
3.1.3 Typing
3.1.4 Integer arithmetic and machine integers
3.1.5 Real numbers and floating point numbers
3.2 Simple contracts
3.3 Behavior clauses
3.4 Code annotations
3.4.1 Assertions
3.4.2 Loop annotations
3.5 Data invariants
3.6 Advanced modeling language
3.6.1 Logic definitions
3.6.2 Hybrid predicates
3.6.3 Abstract data types
3.7 Termination
3.7.1 Loop variants
3.8 Ghost variables
Chapter 4 Appendices
4.1 Requirements
4.2 Installation procedure
4.2.1 From the sources
4.2.2 Binaries
4.3 Summary of features and known limitations
4.4 Contacts
Bibliography
Index
