Commit e5cd22e9 authored by Benedikt Becker's avatar Benedikt Becker

Update oracles for api-bench

parent 929aa95b
module M1
use int.Int
goal g: Int.(=) 4 (Int.(+) 2 2)
goal g: Int.( = ) 4 (Int.( + ) 2 2)
end
module M2
......@@ -10,7 +10,7 @@ module M2
let f (x : int)
requires { x = 6 }
ensures { result = 42 } =
Int.(*) x 7
Int.( * ) x 7
end
module M3
......@@ -18,8 +18,8 @@ module M3
use ref.Ref
let f (_ : ())
ensures { Int.(>=) result 0 } =
let x = Ref.ref 42 in Ref.(!) x
ensures { Int.( >= ) result 0 } =
let x = Ref.ref 42 in Ref.( ! ) x
end
module M4
......@@ -27,9 +27,9 @@ module M4
use array.Array
let f (a : Array.array int)
requires { Int.(>=) (Array.length a) 1 }
returns { _ -> (Array.([]) a 0) = 42 } =
Array.([]<-) a 0 42
requires { Int.( >= ) (Array.length a) 1 }
returns { _ -> (Array.( [] ) a 0) = 42 } =
Array.( []<- ) a 0 42
end
Tasks are:
Task 1: theory Task
......
......@@ -3,10 +3,10 @@ module M1
use ref.Refint
let f (x : ref int)
requires { Int.(<=) (Refint.(!) x) 100 }
returns { _ -> (Refint.(!) x) = 100 } =
while Int.(<) (Refint.(!) x) 100 do
variant { Int.(-) 100 (Refint.(!) x) }
requires { Int.( <= ) (Refint.( ! ) x) 100 }
returns { _ -> (Refint.( ! ) x) = 100 } =
while Int.( < ) (Refint.( ! ) x) 100 do
variant { Int.( - ) 100 (Refint.( ! ) x) }
Refint.incr x
done
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment