Laurel Language Designer Guide

Laurel Language Designer Guide

Table of Contents

1.	Design Goals
2.	Correctness checking features
3.	Prevent duplicate work
4.	Modular Verification
5.	Minimize Verification Code
6.	Automated proof search
7.	Use complete algorithms to reduce workload
8.	Verification code must be erasable
9.	Great user experience
10.	Planned features

5. Minimize Verification Code

5.1.	Transparent procedures
5.2.	Heap mutation in contracts
5.3.	Aliasing helpers
5.4.	Invoke on

5.2. Heap mutation in contracts

←5.1. Transparent procedures 5.3. Aliasing helpers→

5.2. Heap mutation in contracts🔗

Feature described in the Planned features section.

←5.1. Transparent procedures 5.3. Aliasing helpers→