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
|
module Exception1
[@java:exception:Exception]
use mach.java.lang.Integer
type t = { value : integer; d : bool }
exception E1 t
let crt[@java:constructor] (i : integer) : t =
{ value = i; d = false }
end
module Exception2
[@java:exception:Exception]
use mach.java.lang.Integer
type t = { value : integer; d : bool }
exception E2 t
let crt[@java:constructor] (i : integer) : t =
{ value = i; d = false }
end
module ExceptionThrow
use Exception1
use Exception2
use mach.java.lang.Integer
use mach.java.lang.IndexOutOfBoundsException
use mach.java.util.NoSuchElementException
let func (i : integer) : integer
ensures { result = i }
raises { Exception1.E1 v -> (Exception1.value v = i) && (i = 0) }
raises { Exception2.E2 v -> (Exception2.value v = i) && (i = 1) }
raises { IndexOutOfBoundsException.E -> i = 2 }
raises { NoSuchElementException.E -> i = 3 }
=
if i = 0 then raise Exception1.E1 (Exception1.crt i);
if i = 1 then raise Exception2.E2 (Exception2.crt i);
if i = 2 then raise IndexOutOfBoundsException.E;
if i = 3 then raise NoSuchElementException.E;
i
end
module ExceptionCatch
use mach.java.lang.Integer
use Exception1
use Exception2
use mach.java.lang.IndexOutOfBoundsException
use mach.java.util.NoSuchElementException
use ExceptionThrow
let no_raise (i : integer) : integer
requires { i <> 1 }
ensures { result = i }
raises { Exception1.E1 v -> (Exception1.value v = i) && (i = 0) }
=
try
func i
with
Exception2.E2 _ -> absurd
| IndexOutOfBoundsException.E -> i
| NoSuchElementException.E -> i
end
end
|
