tests/label.mlw

   1
   2 module M
   3
   4   use module ref.Ref
   5
   6   val x: ref int
   7
   8   let f () =
   9      x := 1;
  10      'L1:
  11      x := 2;
  12      'L2:
  13      x := 3;
  14      assert { (at !x 'L1) = 1 /\ (at !x 'L2) = 2 /\
  15               (at (at !x 'L1) 'L2) = 1 /\
  16               (at (at !x 'L2) 'L1) = 2 }
  17
  18 end
  19