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
78
79
80
81
82
83
84
85
86
87
|
module Employee
use mach.java.lang.Integer
use mach.java.lang.String
type service_id = HUMAN_RES | TECHNICAL | BUSINESS
type t = {
name: string;
room: integer;
phone : string;
service : service_id;
}
let create_employee [@java:constructor] (name : string) (room : integer) (phone : string)
(service : service_id) = {
name = name; room = room; phone = phone; service = service;
}
end
module Directory
use int.Int
use mach.java.lang.String
use mach.java.lang.Integer
use mach.java.util.Map
use Employee
type t [@extraction:preserve_single_field]= {
employees [@java:visibility:private] : Map.map string Employee.t
}
let create_directory [@java:constructor] () : t = {
employees = Map.empty()
}
let add_employee (self : t) (name : string) (phone : string) (room : integer)
(service : service_id) : unit
requires { not Map.containsKey self.employees name }
ensures { Map.containsKey self.employees name }
ensures { let m = Map.get self.employees name in
m.name = name && m.phone = phone && m.room = room && m.service = service }
=
Map.put self.employees name (Employee.create_employee name room phone service)
end
module EmployeeAlreadyExistsException [@java:exception:RuntimeException]
use mach.java.lang.String
type t [@extraction:preserve_single_field] = { msg : string }
exception E t
let constructor[@java:constructor](name : string) : t = {
msg = (String.format_1 "Employee '%s' already exists" name)
}
let getMessage(self : t) : string = self.msg
end
module CheckedDirectory
use int.Int
use mach.java.lang.String
use mach.java.lang.Integer
use mach.java.util.Map
use Employee
use EmployeeAlreadyExistsException
type t [@extraction:preserve_single_field]= {
employees [@java:visibility:private] : Map.map string Employee.t
}
let create_directory [@java:constructor] () : t = {
employees = Map.empty()
}
let add_employee (self : t) (name : string) (phone : string) (room : integer)
(service : service_id) : unit
ensures { Map.containsKey self.employees name }
ensures { let m = Map.get self.employees name in
m.name = name && m.phone = phone && m.room = room && m.service = service }
raises { EmployeeAlreadyExistsException.E _ -> Map.containsKey (old self.employees) name }
=
if Map.containsKey self.employees name then
raise (EmployeeAlreadyExistsException.E (constructor name));
Map.put self.employees name (Employee.create_employee name room phone service)
end
|
