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.
Coroutines
11.
Planned features
11.
Planned features
11.1.
Dynamic type
11.2.
Type inference
11.3.
Flow based types
11.4.
Global variables
11.5.
Non-determinism
11.6.
Immutable fields
11.7.
Reads clauses
11.8.
Frozen types
11.9.
Enhance support for transparent procedures
11.10.
Property-based testing
11.11.
Data-flow analysis
11.12.
Heap mutation in contracts
11.13.
Proof By
11.14.
Inference of composite types
11.15.
Decreases clauses
11.16.
Exception inference
11.11.
Data-flow analysis
←
11.10. Property-based testing
11.12. Heap mutation in contracts
→
11.11. Data-flow analysis
🔗
To be designed..
←
11.10. Property-based testing
11.12. Heap mutation in contracts
→