[Spark2014-discuss] [M503-001] SPARK 2014: proof rules for type invariants
duff at adacore.com
Tue May 7 18:15:58 CEST 2013
Patrice Chalin <chalin at santoslab.org> wrote:
>... I don't know how constructors show up in Ada, ...
A function returning type T can be thought of as a constructor for type T.
Ada doesn't have any specific "constructor" feature as in C++ et al.
> p.s. Has some thought been given to package invariants?
The ARG did consider package invariants, but they didn't make it into
Ada 2012. I don't see any information in the AI's explaining why they
were left out. Probably just because it's one more feature to be added
to a language that already has too many features.
More information about the Spark2014-discuss