5. Verification - Fundamentals🔗

A verification feature may be erased or approximated when a program is run concretely: assume is a no-op in the interpreter, modifies is not checked, and a contract on a bodiless procedure has no runtime meaning at all. Its behaviour under verification is therefore the behaviour that matters.

This section covers the features that do not involve the heap, which are enough to specify code over plain values.

1. 5.1. Assertions
2. 5.2. Erased code
3. 5.3. Loop invariants
4. 5.4. Preconditions
5. 5.5. Postconditions
6. 5.6. Contract modes: free and checked
7. 5.7. Contract well-formedness
8. 5.8. Naming a failure with summary
9. 5.9. Quantifier
10. 5.10. Lemmas with invokeOn
11. 5.11. Termination checking
12. 5.12. Constrained types