Ola Fosheim Grøstad:
Ada with SPARK 2014 makes D look like it is stuck in the 80s:
4.2. Subprogram Contracts
4.2.1. Preconditions
4.2.2. Postconditions
4.2.3. Contract Cases
4.2.4. Data Dependencies
4.2.5. Flow Dependencies
4.2.6. State Abstraction and Contracts
4.2.6.1. State Abstraction and Dependencies
4.2.6.2. State Abstraction and Functional Contracts
4.3. Package Contracts
4.3.1. State Abstraction
4.3.2. Package Initialization
4.3.3. Package Initial Condition
4.3.4. Interfaces to the Physical World
4.3.4.1. Volatile Variables
4.3.4.2. Flavors of Volatile Variables
4.3.4.3. External State Abstraction
4.4. Type Contracts
4.4.1. Scalar Ranges
4.4.2. Static Predicates
4.4.3. Record Discriminants
4.4.4. Default Initial Condition
4.5. Specification Features
4.5.1. Attribute Old
4.5.1.1. In a Postcondition
4.5.1.2. In Contract Cases
4.5.1.3. In a Potentially Unevaluated Expression
4.5.2. Attribute Result
4.5.3. Attribute Loop_Entry
4.5.4. Attribute Update
4.5.5. Conditional Expressions
4.5.6. Quantified Expressions
4.5.7. Expression Functions
4.5.8. Ghost Code
4.5.8.1. Ghost Functions
4.5.8.2. Ghost Variables
Case 1: Keeping Intermediate Values
Case 2: Keeping Memory of Previous State
Case 3: Logging Previous Events
4.5.8.3. Ghost Types
4.5.8.4. Ghost Procedures
4.5.8.5. Ghost Packages
4.5.8.6. Imported Ghost Subprograms
4.6. Assertion Pragmas
4.6.1. Pragma Assert
4.6.2. Loop Invariants
4.6.3. Loop Variants
4.6.4. Pragma Assume
4.6.5. Pragma Assert_And_Cut
That seems a bit too much for the average human to handle :-)
Sometimes features help, but that list seems excessive for a
language that is not meant for high integrity systems as D.
Bye,
bearophile
