ANSWER TO MOCK QUESTION 1: Note that I'm writing x=y as shorthand for (x=y ∧ emp), etc. { lseg(x,null) ∗ lseg(y,null) } if (x=null) { { lseg(y,null) } x := y; { lseg(x,null)} } else { { lseg(x,null) ∗ x≠null ∗ lseg(y,null) } { lseg(x,x) ∗ lseg(x,null) ∗ x≠null ∗ lseg(y,null) } t := x; { lseg(x,t) ∗ lseg(t,null) ∗ t≠null ∗ lseg(y,null) } { ∃u. lseg(x,t) ∗ t↦u ∗ lseg(u,null) ∗ lseg(y,null) } u := [t]; { lseg(x,t) ∗ t↦u ∗ lseg(u,null) ∗ lseg(y,null) } // begin frame { lseg(x,t) ∗ t↦u ∗ lseg(u,null) } while (u≠null) { { lseg(x,t) ∗ t↦u ∗ lseg(u,null) ∗ u≠null } { lseg(x,u) ∗ lseg(u,null) ∗ u≠null } t := u; { lseg(x,t) ∗ lseg(t,null) ∗ t≠null } { ∃u. lseg(x,t) ∗ t↦u ∗ lseg(u,null) } u := [t]; { lseg(x,t) ∗ t↦u ∗ lseg(u,null) } } { lseg(x,t) ∗ t↦null } [t] := y; { lseg(x,t) ∗ t↦y } // end frame { lseg(x,t) ∗ t↦y ∗ lseg(y,null) } { lseg(x,null) } } { lseg(x,null) }