Solution for Basic.triple_inplace_double
Lemma triple_inplace_double : forall (p:loc) (n:int),
triple (inplace_double p)
(p ~~> n)
(fun _ => p ~~> (2*n)).
Proof.
xwp. xapp. xapp. xapp. xsimpl. math.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback