297
(a) §
(b) §
In a language with array element assignment, the program x:=i. i:=Ai. Ai:=x
was written with the intention to swap the values of i and A i . Assume that all variables and array elements are of type nat , and that i has a value that is an index of A.
Invariables x, i,and A,specifythat i and Ai shouldbeswapped,therestof A should be unchanged, but x might change.
iʹ=Ai ∧ Aʹ=i→i|A
Find the exact precondition for which the program refines the specification of part (a). ∀xʹ, iʹ, Aʹ· iʹ=Ai ∧ Aʹ = i→i | A ⇐ (x:= i. i:= Ai. A:= i→x | A) expand final asmt
= ∀xʹ,iʹ,Aʹ·iʹ=Ai ∧ Aʹ=i→i|A ⇐ (x:=i. i:=Ai. xʹ=x∧iʹ=i∧Aʹ=i→x|A) substitution law twice
= ∀xʹ,iʹ,Aʹ·iʹ=Ai ∧ Aʹ=i→i|A ⇐ xʹ=i∧iʹ=Ai ∧ Aʹ=Ai→i|A 1-pt×3
= Ai=i
= Ai=i
= Ai=i
= Ai=i
= Ai=i Soiand making the
(c) §
Find the exact postcondition for which the program refines the specification of part (a). ∀x,i,A·iʹ=Ai ∧ Aʹ=i→i|A ⇐ xʹ=i∧iʹ=Ai ∧ Aʹ=Ai→i|A
context to drop first iʹ=Ai ; x doesn’t appear; one-pt for i ; context to replace last Ai
= Ai=Ai ∧ Ai→i | A = i→i | A
= Ai→i | A = i→i | A
= if Ai = i then Ai→i | A = i→i | A else Ai→i | A
= ifAi=ithen⊤elseAi→i|A = i→i|Afi
reflexivity and identity case idempotent context, reflexive OneCaseLaw listequality split domain of j Theleftdisjunct Ai=i gives usthecontext Ai⧧i in the right disjunct. Use it to simplify (Ai→i | A)i . Also simplify (i→i | A)i .
∨ ( Ai = i
∧ ∀j· j⧧i ⇒ (Ai→i | A)j = (i→i | A)j ) absorption
A i will be swapped if and only if they have the same value to start with, swap useless.
∨ Ai→i|A = i→i|A
∨ ∀j· (Ai→i | A)j = (i→i | A)j ∨ ( (Ai→i|A)i = (i→i|A)i
∧ ∀j·j⧧i ⇒ (Ai→i|A)j = (i→i|A)j )
= ∀A·Aʹ=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|A
= ifxʹ=iʹthen∀A·Aʹ=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|A
else∀A·Aʹ=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|Afi
= ifxʹ=iʹthen∀A·Aʹ=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=xʹ→xʹ|A
caseidempotent context:replace iʹ context:replace Aʹ specialization
else∀A·iʹ→xʹ|A=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|Afi
= xʹ⧧iʹ ⇒ (∀A·iʹ→xʹ|A=xʹ→xʹ|A ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|A)
= xʹ⧧iʹ ⇒ (∀A· xʹ=Aiʹ ∧ Axʹ=xʹ ⇐ iʹ=Axʹ ∧ Aʹ = iʹ→ xʹ | A) context
= xʹ⧧iʹ ⇒ (∀A·⊥ ⇐ iʹ=Axʹ ∧ Aʹ=iʹ→xʹ|A)
notethat xʹ⧧iʹ ∧ Aʹ=iʹ→xʹ|A ⇒ Aʹxʹ=Axʹ
= xʹ⧧iʹ ⇒ (∀A·⊥ ⇐ iʹ=Aʹxʹ ∧ Aʹ=iʹ→xʹ|A)
= xʹ⧧iʹ∧iʹ=Aʹxʹ⇒ ¬(∃A·Aʹ=iʹ→xʹ|A)
= xʹ⧧iʹ ∧ iʹ=Aʹxʹ ⇒ ¬(Aʹiʹ=xʹ)
= xʹ=iʹ ∨ Aʹxʹ⧧iʹ ∨ Aʹiʹ⧧xʹ
If, in the end, we see xʹ=iʹ or Aʹxʹ⧧iʹ or Aʹiʹ⧧xʹ we know they were swapped (well, we won’t see Aʹiʹ⧧xʹ because of the final assignment, so really it’s just the first two possibilities).
=
i→i | A fi