examples/bts/353.mlw

   1
   2 module M
   3
   4   use int.Int
   5   use ref.Ref
   6
   7   let f (a: ref int)
   8     requires { !a = 42 }
   9     ensures { !a = 2 + old !a + result } =
  10     a := 0;
  11     a := 1;
  12     !a+1
  13
  14   let g (a: ref int)
  15     requires { !a = 42 }
  16     ensures { !a = 2 + old !a + result } =
  17     a := 0;
  18     a := 1;
  19     let b = !a + !a in
  20     b+1
  21
  22 end