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
6.
Verification - Objects
6.1.
Modifies clauses
6.2.
Aliasing and separation
6.3.
Reads clauses
6.4.
Old
6.5.
Allocated and fresh
6.6.
Immutable fields
6.7.
Type invariants
6.3.
Reads clauses
←
6.2. Aliasing and separation
6.4. Old
→
6.3. Reads clauses
🔗
To be designed..
Reads clauses can only be specified for deterministic procedures
←
6.2. Aliasing and separation
6.4. Old
→