why3/bench/programs/good/set.mlw

module M

  use int.Int
  use ref.Ref

  (* side effects in tests *)

  val x : ref int

  val set_and_test_zero (v:int) : bool writes {x}
    ensures { !x = v /\ if result=True then !x = 0 else !x <> 0 }

  let p () ensures { result = 1 }
  = if set_and_test_zero 0 then 1 else 2

  val set_and_test_nzero (v:int) : bool writes {x}
    ensures { !x = v /\ if result=True then !x <> 0 else !x = 0 }

  let p2 (y:ref int)
    requires { !y >= 0 }
    ensures  { !y = 0 }
  = while set_and_test_nzero !y do
      invariant { !y >= 0 } variant { !y }
      y := !y - 1
    done

  let p3 (y:ref int)
    requires { !y >= 0 }
    ensures  { !y = 0 }
  = while let b = set_and_test_nzero !y in b do
      invariant { !y >= 0 } variant { !y }
      y := !y - 1
    done

  let p4 (y:ref int)
    requires { !y >= 1 }
    ensures  { !y = 0 }
  = while begin y := !y - 1; (set_and_test_nzero !y) end do
      invariant { !y >= 1 } variant { !y }
      ()
    done

end