mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
19 lines
239 B
Plaintext
19 lines
239 B
Plaintext
|
|
use int.Int
|
|
|
|
val function f (x:int) : int
|
|
|
|
let main_f (y:int) : int
|
|
ensures { result <> 42 }
|
|
=
|
|
f y
|
|
|
|
val function g(x:int) : int
|
|
|
|
axiom g_def : forall x. g x = x+1
|
|
|
|
let main_g (y:int)
|
|
ensures { result <> 44 }
|
|
=
|
|
let z = g y in
|
|
z+1 |