Re: specification logic

To: sbsvax!sieber@fb10vax.sbsvax
Subject: Re: specification logic
From: rdt%QUCIS.BITNET@MITVMA.MIT.EDU
Date: Thu, 9 Jun 88 13:02:04 EDT
Cc: john.reynolds@theory.cs.cmu.edu, oles@ibm.com, types@theory.lcs.mit.edu
        From: "Kurt Sieber" <sieber%fb10vax.sbsvax@sbsvax.uucp>
        Date: Thu, 9 Jun 88 15:35:44 +0200 (MET dst)
        To: rdt@qucis.uucp
        In-Reply-To: rdt%QUCIS.BITNET@unido.uucp's message of Wed, 8 Jun 88 13:5
        Subject:  specification logic

        'Small point': I really meant what I wrote
            (all c,Q. {x=c} Q {x=c+1} => {x=c} P(Q) {x=c+2})
        e.g. the following P satisfies my specification, but not yours

        procedure P(Q):
        begin
        var y;
        y := x;                 % save initial contents of x
        Q;
        if x=y+1 then x:=x+1
        end P;

        My specification is a bit weird, but the problem was, that I didn't
        find a better one, for which I needed the strong constancy axiom.
        (Can you say a bit more precisely what the problem with binary
        search is ?)


The application of Strong Constancy I outlined is, in more detail, as follows.
Let C be binary search of array A.  Let R be the assertion that A is
sorted.  Let (P AND R) and (Q AND R) be the pre and post-conditions,
respectively for C; i.e., one would normally verify C by proving
{P AND R} C {Q AND R}.  But it is evident that C#R (because there are
no assignments to A in C).  Then Strong Constancy allows a reduction of
the verification problem to {P} C {Q}, while still allowing R to be
used wherever necessary.  In effect, R has been "factored out"
of the pre and post-conditions.  The benefit is convenience: instead
of having to carry R through the verification of C, it is simply
available for use as a static assertion, like mathematical facts.
This convenience becomes more significant as programs get larger.

        As far as I remember, I've also worked out Reynolds' example for
        non-interference composition, and I got rid of his problems (i.e. I
        only needed classically valid axioms) by using value identifiers.

        What I wanted to say, is that one does not NEED arguments like
            G#P1 & G#P2 => G#(P1 op P2)
        because most of these non-interference formulas disappear, when we use
        STATE INDEPENDENT formulas.  Of course this is only a vague
        conjecture (I don't have a completeness result !), but at least I
        haven't seen an example so far, which convinced me that these
        nonclassical axioms are necessary or at least useful.

        Regards Kurt.

I don't understand what you mean by "state-independent formulas".
Are you talking about assertions or specifications?

Regards,  Bob.