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) }