[Spark2014-discuss] [M503-001] SPARK 2014: proof rules for type invariants

Bob Duff 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.

- Bob

More information about the Spark2014-discuss mailing list