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

Steve Baird baird at adacore.com
Fri May 17 18:43:11 CEST 2013

On 05/17/2013 02:33 AM, Yannick Moy wrote:
> 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)

And we do have an idiom available that may be useful in the first
release. The following is an excerpt from a message sent to the
spark mailing list (M329-027, 03/29/2013).

   -- Steve


Possibly useful idiom for expressing invariant for a package that has state:

   Given a package with state, as in

     package Pkg is
       procedure Op1 (...);
       procedure Op2 (...);
       procedure OpN (...);
     end Pkg;

     package body Pkg is
       X : T1; Y : T2; Z : T3;
     end Pkg;

we can leave the spec unchanged and
rewrite the body as a wrapper on a
nested package which exports a private
state type which is subject to an invariant,
as in

    package body Pkg is
      package Inner is
        type State is private;
        procedure Op1 (S : in out State; ...);
        procedure Op2 (S : in out State; ...);
        procedure OpN (S : in out State; ...);
        type State
          with Invariant => ...
          is record
            X : T1; Y : T2; Z : T3;
          end record;
      end Inner;

      S : Inner.State; -- the one and only object of this
                       -- type that will ever exist

      procedure OpN (...) is
        Inner.OpN (S, ...);
    end Pkg;

More information about the Spark2014-discuss mailing list