Re: SPARK Question

["Randy Brukardt" <randy@rrsoftware.com>]

<phil.clayton@lineone.net> wrote in message 
news:68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com...
On Tuesday, 7 May 2013 21:44:12 UTC+1, Randy Brukardt wrote:
...
>> Similarly, postconditions often include conditions that hold true after 
>> the
>> call, and it's quite common for those conditions to feed into following
>> preconditions (as in Post => Is_Open(File) after a call to Open). So, as
>> much as possible, postconditions should use the same functions that are 
>> used
>> in preconditions. (The more that's done, the more likely that the 
>> compiler
>> can completely eliminate the pre- and post- condition checks even when
>> they're turned on.)

>Addressing the last paragraph above, the basis of the point is that reusing 
>the
>same syntactic form of predicate in pre- and postconditions makes it easy 
>for a
>compiler to spot that a predicate is a consequence of an earlier predicate. 
>I
>certainly agree with that!  But surely this would allow only the 
>_subsequent_
>occurrences of the predicate to be optimized out?  Above, you seem to 
>suggest
>that both the initial and subsequent occurrence of a predicate can be 
>optimized out.

You're right that only the "subsequent" occurrences can be optimized out - 
but, in well-designed abstractions, the initial state also has a well-known 
set of predicates. This might be hard to model in Ada 2012, although 
invariants certainly would help. Starting out with undefined properties is 
not a good idea, so the only issue is whether there is a clear way to 
communicate that.

For instance, a file starts out with Is_Open = False. The compiler and 
static analyzer need to know this! It's too late to wait until Open is 
called.

> In the example above example, it may be possible for the initial 
> occurrence,
> the postcondition Is_Open(File) of subprogram Open, to be optimized out
> but that is surely for different reasons - the compiler having special 
> knowledge
> about the subprogram Open.

Postconditions get optimized out based on the actual contents of the body. 
This sort of optimization should be trivial (it is made with complete 
knowledge of the implementation, presuming the implementation is contained 
in a single package body, which normally should be the case). At the call 
site, they're assumptions (they've either been checked or proved, either way 
you don't need to recheck them).

> In general, for user-defined subprograms, determining statically whether a
> predicate P(X) holds is, in general, difficult.  Once established, it is
> straightforward to use the theorem  P(X) ? P(X)
> to establish that subsequent occurrences of the same form hold.

It's certainly true "in general", where predicate contents include functions 
with and depending on side-effects, where the initial state of objects is 
not defined, where privacy is not used properly. But why should we care 
about the optimization and performance of poorly designed software?

> Separately, even when reusing the same syntactic form of predicate in
> pre- and postconditions, optimizing out subsequent occurrences of the
> predicate may not be possible as often as one would hope.  Given two
> occurrences of the predicate P(X), to establish that the subsequent
> occurrence holds, it necessary (for the theorem above) to establish that
> the X is the same in both occurrences.  In the case that X is visible
> outside its package and between the two occurrences of P(X) there is
> a call to a subprogram in another package, I can't see how a compiler
> would know that X won't be changed.  (I'm assuming that compilers
> don't look at the bodies of other packages when compiling a package.)
> To avoid such issues, formal methods tools typically require
> subprograms to have a 'frame' annotation that indicates which variables
> a subprogram may change.

First of all, compilers do this all the time. Any compiler that takes 
advantage of 10.2.1(18/3) [and most do] have been doing this for many years. 
In addition, this is essentially the same problem as identifying common 
subexpressions, a problem that optimizers have been doing since the 
beginning of (computer) time. So there is absolutely nothing new here. (The 
only part of this that would be new in Janus/Ada is the idea of assumptions, 
and that fits in very well with our existing optimization technology.)

Secondly, one hopes that most that "predicates" are good, that is that they 
don't violate the Implementation Permission 11.4.2(27/3). One also hopes 
that most objects are of private types and are not modified "out-of-band" 
(whether this is possible is determinable from the declaration of the type, 
so it doesn't require looking into bodies to figure out - ignoring Chapter 
13 effects of course, which are usually erroneous if they have this sort of 
effect). And I'm assuming that function side-effects are declared somehow. 
(Without these things, you can't do any call optimizations without either 
looking in bodies or appealing to the Pure permissions of 10.2.1 - which are 
rarely applicable.)

I agree that Ada 2012 doesn't go far enough to define these things. The 
global in/global out contracts that we worked on but ended up abandoning as 
insufficiently fully baked certainly would have helped a lot.

We actually tried to come up with a rule for 11.4.2 that would have allowed 
such optimizations in all cases (that is certainly the intent -- that 
"assertions" that contain any sort of side-effects are bad). We didn't put 
it into the Standard because we weren't able to draft one that didn't throw 
out good things with the bad. But the intent is still there, and it's 
possible that such a rule (a version 10.2.1(18) for 11.4.2) will appear in 
the future.

>So, in summary, optimizing out predicates in pre- and postconditions may 
>not be that easy.

That's probably true in Ada 2012, especially if you don't use 
implementation-defined stuff like Pure_Function (in GNAT). That's why I was 
babbling about an Ada-like language with an extension to constraints that 
could carry the missing information. Perhaps there is a way to get that 
information into Ada as well (I'm not as sure).

                                                           Randy.