Laurel User Guide

Laurel User Guide

Table of Contents

1.	Summary
2.	Resolution
3.	Execution
4.	Verification - Fundamentals
5.	Verification - Objects
6.	Exceptions
7.	Verification - Proof hints

4. Verification - Fundamentals

4.1.	Assertions
4.2.	Erased code
4.3.	Loop invariants
4.4.	Preconditions
4.5.	Postconditions
4.6.	Quantifier
4.7.	Termination checking
4.8.	Constrained types

4.7. Termination checking

←4.6. Quantifier 4.8. Constrained types→

4.7. Termination checking🔗

To be designed..

←4.6. Quantifier 4.8. Constrained types→