Shadowing (e.g., mutable variables) makes sessions unstable
Open the following script in the IDE, perform split_vc
, then apply trans with x2
. This produces two subgoals; perform apply trans with x1
on the first one. Save the session, restore the assertion, and reload the session. Transformation apply trans with x1
has now moved from the first subgoal to the second one. This happens randomly, so you might have to comment and reload again for it to occur.
type t = { mutable f:int }
predicate p int int
axiom trans: forall a b c. p a b -> p b c -> p a c
val q (x:t): unit
writes { x }
ensures { p x.f (old x.f) }
let foo (x:t)
ensures { p x.f (old x).f }
=
q x;
q x;
q x;
(*assert { true };*)
()
Presumably, this is caused by all the subgoals ending up with the exact same shape:
apV0V2IapV1V2IapV0V1F
apaxax
apply premises
postcondition
apV6V3IapV6V5FIapV5V4FIapV4V3FF
VC for foo
a97120fa31e7091252dd64bd73d61a64 5H4H0
e1d390651f7c12707fca160af9f2c85a 3H1H1H1H1H0
d4e7240950bed98e2516c724019fc9ef 2H1H1H1H1H0
c43c0cfc6afdfd35614f3bb4a51a9d7e 2H1H1H1H1H0
8f803408c1b99aef55c9955b7691760d 2H1H1H1H1H0
28c8a786d26365e6c894c3d9b72f6400 2H1H1H1H1H0