[Spark2014-discuss] [M503-001] SPARK 2014: proof rules for type invariants
moy at adacore.com
Fri May 3 09:11:41 CEST 2013
I'm resending this interesting email from Steve to spark2014-discuss@ (a public mailing list now), which we should more for this kind of language issues form now on. It is fine to use an internal mailing list for details of tools, but the language issues should be discussed broadly.
-- Steve Baird (2013-05-03)
> The runtime checks associated with type invariants are performed
> a the end of a call to a "boundary" subprogram which updates
> an object whose type is subject to an invariant.
> It was observed that the associated proof obligation would
> be difficult to discharge if we didn't also have the invariant as
> a precondition.
> And so we do. An additional proof obligation, not corresponding
> to any Ada-defined runtime check, is defined (see Spark RM
> for details). Otherwise the user would have had to explicitly
> repeat the invariant as a precondition and that would not be good.
> After discussing this with Trevor, it sees like this is only
> a partial solution to the problem. In some sense, we have
> only moved the lump in the rug.
> Suppose we have a type My_Package.My_Type which is subject
> to an invariant.
> A client declares an object of this type and the desired
> invariant is established at that point.
> The client then passes this object as a parameter through
> a long sequence of calls to subprograms outside of My_Package:
> The client calls Aa, which calls Bb, which calls Cc ...
> which calls Zz, which finally calls My_Package.Some_Operation.
> At this point, we have a proof obligation to discharge: the
> aforementioned precondition for the call to Some_Operation.
> To prove this, does Zz need to repeat the precondition as
> a precondition of its own, thereby shifting the burden to Yy?
> If we repeat this process until we get back to Aa, this
> will work. At the point where Aa is called, the invariant
> is known to be true and all is well.
> Except that the precondition has now been explicitly
> copied a large number of times. This is not good, even
> if the invariant is just a call to a function named
> Is_Valid. And it gets worse when we pass around
> objects with components of subject-to-invariant types.
> Am I right in thinking that this is the current
> situation? That is, you can use type invariants, but it can
> rapidly become very burdensome in some cases because
> the invariant will have to be kept track of explicitly.
> Consider, in contrast, how subtypes (including subtypes
> with predicates) work. We have an implicit precondition
> on every subprogram that all parts of all of its inputs
> belong to their respective subtypes and an implicit postcondition
> that the same holds for outputs.
> We'd like to use the same approach for invariants, but there are
> some differences between subtype constraints/predicates and
> 1) it is perfectly ok to violate the
> invariant while one is inside the package.
> 2) The infinite-recursion problem (this can occur with
> subtypes if a predicate is imposed on a first named
> subtype and involves using the current instance in
> way that involves a predicate check, typically
> passing it as a parameter in a call; for subtypes,
> the answer is "don't do that".). Perhaps this
> problem could somehow be finessed because we are
> only talking about proofs and proof obligations here.
> Could we have a different implicit contract for a subprogram
> depending on where the subprogram is declared (i.e., on
> whether it is allowed to break the invariant)?
> I think we could get into some complicated messes with
> the LSP requirements we impose for overriding subprograms
> if we have different implicit contracts for a subprogram
> depending on where it is declared, but I doubt this nasty
> interaction would come up in practice.
> Alternatively, we could tighten up Ada's rules some more
> (we've already tightened them up slightly as described above)
> and treat type invariants just like subtype validity for
> purposes of defining implicit subprogram contracts for
> all subprograms. That would mean that it is ok to violate the
> invariant within a subprogram, but you can't pass an
> invariant-violating-value as a parameter, even to
> a subprogram which is not even visible outside of the
> invariant-maintaining package.
> -- Steve
More information about the Spark2014-discuss