Laurel User Guide

Laurel User Guide

Table of Contents

1.	Summary
2.	Syntax
3.	Resolution
4.	Execution
5.	Verification - Fundamentals
6.	Verification - Objects
7.	Verification - Continued
8.	Verification - Proof hints
9.	Debugging and tooling
10.	Current limitations

5. Verification - Fundamentals

5.1.	Assertions
5.2.	Erased code
5.3.	Loop invariants
5.4.	Preconditions
5.5.	Postconditions
5.6.	Contract modes: `free` and `checked`
5.7.	Contract well-formedness
5.8.	Naming a failure with `summary`
5.9.	Quantifier
5.10.	Lemmas with `invokeOn`
5.11.	Termination checking
5.12.	Constrained types

5.11. Termination checking

←5.10. Lemmas with invokeOn 5.12. Constrained types→

5.11. Termination checking🔗

To be designed..

←5.10. Lemmas with invokeOn 5.12. Constrained types→