423 A binary tree can be stored as a list of nodes in breadth order. Traditionally, the root is at index 1 , the node at index n has its left child at index 2×n and its right child at index 2×n+1 . Suppose the user’s variable is x: X , and the implementer’s variables are s: [*X] and p: nat+1 , and the operations are
goHome = goLeft = goRight = goUp = put = get =
p:= 1
p:= 2×p p:= 2×p + 1 p:=divp2 s:=p→x|s x:=sp
Now suppose we decide to move the entire list down one index so that we do not waste index 0. Therootisatindex 0,itschildrenareatindexes 1 and 2,andsoon. Develop the necessary data transform, and use it to transform the operations.
§ The new implementer’s variables are r: [*X] and q: nat . The transform is r=s[1;..#s] ∧ p=q+1
For each of the transformations, it will be easy enough to eliminate the three variables p , sʹ , and pʹ by one-point. The trick to eliminate s is explained after the transformations.
Transform goHome :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ,pʹ·rʹ=sʹ[1;..#sʹ]∧pʹ=qʹ+1∧xʹ=x∧sʹ=s∧pʹ=1
= xʹ=x ∧ rʹ=r ∧ 1 = qʹ+1
= q:= 0
Transform goLeft :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ, pʹ· rʹ = sʹ[1;..#sʹ] ∧ pʹ = qʹ+1 ∧ xʹ=x ∧ sʹ=s ∧ pʹ=2×p
= xʹ=x ∧ rʹ=r ∧ 2×(q+1) = qʹ+1
= q:= 2×q + 1
Transform goRight :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ, pʹ· rʹ = sʹ[1;..#sʹ] ∧ pʹ = qʹ+1 ∧ xʹ=x ∧ sʹ=s ∧ pʹ=2×p+1
= xʹ=x ∧ rʹ=r ∧ 2×(q+1) + 1 = qʹ+1
= q:= 2×q + 2
Transform goUp :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ,pʹ·rʹ=sʹ[1;..#sʹ]∧pʹ=qʹ+1∧xʹ=x∧sʹ=s∧pʹ=divp2
= xʹ=x ∧ rʹ=r ∧ div (q+1) 2 = qʹ+1
= q:= div (q+1) 2 – 1
= q:= div (q–1) 2
Transform put :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ,pʹ·rʹ=sʹ[1;..#sʹ]∧pʹ=qʹ+1∧xʹ=x∧sʹ=p→x|s∧pʹ=p
= xʹ=x∧rʹ=q→x|r ∧ qʹ+1=q+1
= r:=q→x|r
Transform get :
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ,pʹ·rʹ=sʹ[1;..#sʹ]∧pʹ=qʹ+1∧xʹ=sp∧sʹ=s∧pʹ=p
= xʹ=r q ∧ rʹ=r ∧ qʹ+1=q+1
= x:=rq
To transform put we start with
∀s, p· r = s[1;..#s] ∧ p = q+1
⇒ ∃sʹ,pʹ·rʹ=sʹ[1;..#sʹ]∧pʹ=qʹ+1∧xʹ=x∧sʹ=p→x|s∧pʹ=p
The three variables p , sʹ , and pʹ are easy to eliminate by one-point. We get
= ∀s· r = s[1;..#s] ⇒ rʹ = (q+1→x | s)[1;..#(q+1→x | s)] ∧ q+1 = qʹ+1 ∧ xʹ=x
The problem is to get rid of s because we don’t have s=something . We have r = s[1;..#s]
From this we see that #r = #s–1 and s = [i];;r for some unknown item i . I’ll use that to eliminate s .
= rʹ = (q+1→x | [i];;r)[1;..#(q+1→x | [i];;r)] ∧ q+1 = qʹ+1 ∧ xʹ=x
We can simplify #(q+1→x | [i];;r) ro #r+1 and simplify q+1 = qʹ+1 to qʹ=q . = rʹ = (q+1→x | [i];;r)[1;.. #r+1] ∧ qʹ=q ∧ xʹ=x
Now we need to simplify (q+1→x | [i];;r)[1;.. #r+1] . We have a list (q+1→x | [i];;r) of length #r+1 , and in this list at index q+1 the item is x . Now we index with the list [1;.. #r+1] , which shifts all the indexes down 1 . So now at index q the item is x .
= xʹ=x∧rʹ=q→x|r ∧ qʹ=q = r:=q→x|r
I wish I could see a nice series of formal steps.