mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
32 lines
481 B
Plaintext
32 lines
481 B
Plaintext
module Ce_int32
|
|
|
|
use ref.Ref
|
|
use export mach.int.Int32
|
|
|
|
meta "meta_incremental" ""
|
|
|
|
let dummy_update (r: ref int32)
|
|
requires { to_int !r = 22}
|
|
ensures {to_int !r = 42} =
|
|
r := of_int 42;
|
|
r := !r + !r;
|
|
|
|
end
|
|
|
|
|
|
module Ce_interesting
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
use export mach.int.Int32
|
|
|
|
meta "meta_incremental" ""
|
|
|
|
let dummy_update (r: ref int32)
|
|
requires { to_int !r > 22}
|
|
ensures {to_int !r <= 42} =
|
|
r := of_int 42;
|
|
r := !r + !r;
|
|
|
|
end
|