1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
module M1
use int.Int
goal g: Int.( = ) 4 (Int.( + ) 2 2)
end
module M2
use int.Int
let f (x : int)
requires { x = 6 }
ensures { result = 42 }
= Int.( * ) x 7
end
module M3
use int.Int
use ref.Ref
let f (_ : ())
ensures { Int.( >= ) result 0 }
= let x = Ref.ref 42 in Ref.( ! ) x
end
module M4
use int.Int
use array.Array
let f (a : Array.array int)
requires { Int.( >= ) (a.Array.length) 1 }
writes { a }
ensures { (Array.( [] ) a 0) = 42 }
= Array.( []<- ) a 0 42
end
module Mglob
use int.Int
let ref x = any int
let f (_ : ())
writes { x [@mlw:reference_var] }
= (x [@mlw:reference_var]) <- (Int.( + ) x [@mlw:reference_var] 1)
end
module Mscope
use int.Int
scope S
function f (x: int) : int = x
end
import S
goal g: Int.( = ) (2.f) 2
end
module M5
use int.Int
use array.Array
let f (a : Array.array int)
requires { Int.( >= ) (a.Array.length) 1 }
ensures { (Array.( [] ) a 0) = 42 }
= Array.( []<- ) a 0 42
end
module M6
use int.Int
use array.Array
let f (a : Array.array int)
requires { Int.( >= ) (a.Array.length) 1 }
ensures { (Array.( [] ) a 0) = 42 }
= Array.( []<- ) a 0 42
end
On task 1, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 2, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 3, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 4, alt-ergo answers Valid (<hidden>s, <hidden> steps)
|
