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

Yannick Moy moy at adacore.com
Fri May 17 11:33:56 CEST 2013


-- Patrice Chalin (2013-05-07)
> I generally agree with what Yannick has written. I did want to point out that JML has special rules (re. invariants) for both "helper methods" and constructors, "9.6.4 Semantics of helper methods and constructors" - http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_9.html#SEC98 
> 
> The idea was that helper methods are used by constructors to assist in performing object initialization.  I don't know how constructors show up in Ada, nor whether you think that the concept of a helper routine would be useful.  The point is that if you have rules that implicitly add invariants to pre and/or post conditions, one will inevitably come to a situation where you want to turn that off.

Hi Patrice,

The mechanism for type invariants in Ada 2012 already makes room for helper subprograms. It says:

"An invariant is checked upon successful return from a call on any subprogram or entry that [..] is visible outside the immediate scope of type T or overrides an operation that is visible outside the  immediate scope of T [..]"

So all helper subprograms defined in the body of the unit, or the private part of the spec, have no such checks attached. Only subprograms which form part of the API (in the visible part of the spec) have invariant checks attached.

> p.s. Has some thought been given to package invariants?


As Bob said, ARG did not pursue this further. You can look at the discussion there:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0146-1.txt?rev=1.15

(Look for "package invariant")

Package invariants were rejected because "they didn't seem to add sufficient benefit over simply using postconditions". This is understandable that, from a run-time point-of-view, that's indeed the case. But if we also target formal verification with SPARK, package invariant make much more sense. This would not preclude a run-time checking that adds them to postconditions. So something to consider for SPARK 2014. (but not for the first release)
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list