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

10. Planned features

10.1.	Dynamic type
10.2.	Type inference
10.3.	Flow based types
10.4.	Global variables
10.5.	Non-determinism
10.6.	Immutable fields
10.7.	Reads clauses
10.8.	Frozen types
10.9.	Enhance support for transparent procedures
10.10.	Property-based testing
10.11.	Data-flow analysis
10.12.	Heap mutation in contracts
10.13.	Proof By
10.14.	Inference of composite types
10.15.	Decreases clauses
10.16.	Exception inference

10.15. Decreases clauses

←10.14. Inference of composite types 10.16. Exception inference→

10.15. Decreases clauses🔗

To enable proving that contracts terminate, Laurel uses decreases clauses to enable proving the termination of procedure calls.

←10.14. Inference of composite types 10.16. Exception inference→