Contracts
Sections
- Overview
- Basic Aspects of Deductive Program Reasoning in Slang/Logika
- Assertions and Basic Property/Constraint Expressions
- Quantification
- Assume
- Loop Invariants
- Method Contracts Basics
- Assume / Guarantee Reasoning
- Omitting Sections of a Method Contract
- Using Contracts to Capture Important Properties Rather Than Full Behavior
- Contract Cases
- Contracts Dealing with Data Structures
- Specification-only Methods
- Discussion and Application Concepts
- Extended Example -- Circular Queue