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

5. Verification - Objects

5.1.	Modifies clauses
5.2.	Reads clauses
5.3.	Old
5.4.	Allocated and fresh
5.5.	Immutable fields
5.6.	Type invariants
5.7.	Concurrency

5.7. Concurrency

←5.6. Type invariants 6. Exceptions→

5.7. Concurrency🔗

To be designed..

←5.6. Type invariants 6. Exceptions→