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.10.
Property-based testing
←
10.9. Enhance support for transparent procedures
10.11. Data-flow analysis
→
10.10. Property-based testing
🔗
To be designed..
←
10.9. Enhance support for transparent procedures
10.11. Data-flow analysis
→