[CST-2] Spec & Ver I

[M.Y.W.Y. Becker]

--On 31 May 2001 15:40 +0100 Rob Newsome <rln23@cam.ac.uk> wrote:

> 1999 Paper 8 Question 2...
>
> Explain how to translate this into higher-oder logic:
>
> {X=x & Y=y} TEMP:=X; X:=Y; y:=TEMP {X=y & Y=x}
                            ^^^
                          should be a Y I guess

Translation function denoted by [[...]]:


  [[{X=x & Y=y} TEMP:=X; X:=Y; Y:=TEMP {X=y & Y=x}]]
= Spec([[X=x&Y=y]],[[TEMP:=X; X:=Y; Y=TEMP]], [[{X=y & Y=x}]])

with
  Spec(P,C,Q)
= Forall s1,s2: P s1 & C(s1,s2) => Q s2

  [[X=x & Y=y]]
= Lambda s: s'X'=x & s'Y'=y

and similarly for the postcondition.
Now the command itself:

  [[TEMP:=X; X:=Y; Y:=TEMP]]
= Seq(Assign('TEMP','X'),Seq(Assign('X','Y'),Assign('Y','TEMP'))

with
  Seq(C1,C2) = Lambda s1,s2: Exists s3: C1(s1,s3) & C2(s3,s2)
  Assign(P,Q) = Lambda s1,s2: s2=Lambda str: (str=P) -> s1 Q | s1 str


Mo