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
|
module MutRec
use int.Int
use int.EuclideanDivision
use mach.java.lang.ArithmeticException
use mach.java.lang.String
use mach.java.lang.Integer
use mach.java.util.Random
use mach.java.lang.Array
let rec even (number : integer) : bool
ensures { result <-> mod number 2 = 0 }
variant { if number < 0 then -number else number }
=
if number = 0 then true
else if number < 0 then odd (number + 1)
else odd (number - 1)
with odd (number : integer) : bool
ensures { result <-> mod number 2 = 1 }
variant { if number < 0 then -number else number }
=
if number = 0 then false
else if number < 0 then even (number + 1)
else even (number - 1)
let main (array string) : unit =
try
let rnd = Random.create () in
for i = 0:integer to 100:integer do
let b = Random.next_bounded_int rnd 72 in
if (b % 2 = 0 && odd b) || (b % 2 = 1 && even b) then
raise ArithmeticException.E
done
with
| IllegalArgumentException.E -> absurd
| ArithmeticException.E -> absurd
end
end
|
