[CST-2] 98-8-1 spec and vec 1

[M.Y.W.Y. Becker]

--On 17 May 2001 18:47 +0100 Sapna Jethwa <spj23@hermes.cam.ac.uk> wrote:
>for 98-8-1 question :
>
> could someone tell me what the 2 annotations after the DO commands are
> meant to be? I think the second one is FACT = n!/Y! but i'm not sure and

The first one could be e.g.
n>=0 & n!=FACT*N! & N>=0

and the second
n>=0 & N>1 & Y>=1 & FACT=X(N-Y+1) & n!=XN!

and you'll get 7 rather trivial VCs.

Note that it is almost always the case that invariants are made up of 3 
parts:
(i) facts carried over from previous command:
    n>=0 for the first invariant and n>=0 & N>1 for the second
(ii) extra constraints on the guard of the loop:
     N>=0 and Y>=1, respectively
(iii) "real" invariant properties obtained by looking at table of values:
      n!=FACT*N! and FACT=X(N-Y+1) & n!=XN!, respectively

Mostly, not all of these parts are absolutely essential but it's safer to 
put them in at the beginning unless you don't mind correcting the invariant 
during the proof.


Moritz