# Re: specification logic

```        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.

```