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.2. Reads clauses

←5.1. Modifies clauses 5.3. Old→

5.2. Reads clauses🔗

To be designed..

Reads clauses can only be specified for deterministic procedures

←5.1. Modifies clauses 5.3. Old→