-
Notifications
You must be signed in to change notification settings - Fork 0
/
counter.mlw
64 lines (41 loc) · 1.27 KB
/
counter.mlw
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
(* Abstract specification of a concurrent shared memory counter, assuming atomic updates
*)
module Counter
use export int.Int
use export map.Map
use export map.Const
type state = Start | Done
type thread
(* System configurations
*)
type world = { pc : map thread state ; counter : int }
(* Inductive invariant
*)
predicate inv (w:world) = w.counter >= 0
(* System INIT
*)
predicate initWorld_p (w:world) = w.pc = const Start /\ w.counter=0
let ghost predicate initWorld (w:world) = initWorld_p w
(* System action
*)
predicate trans_enbld (w:world) (t:thread) =
w.pc[t] = Start
let ghost function trans (w:world) (t:thread) : world
requires { trans_enbld w t }
ensures { inv w -> inv result }
= { pc = set (w.pc) t Done ; counter = w.counter+1 }
(* Transition relation
*)
inductive stepind world world =
| trans : forall w :world, t :thread.
trans_enbld w t -> stepind w (trans w t )
let ghost predicate step (w1:world) (w2:world) = stepind w1 w2
(* Proof of inductiveness, if desired
*)
(* clone export core.Inductiveness with *)
(* type world, *)
(* predicate inv, *)
(* val step, *)
(* val initWorld *)
(* lemma safety : forall w :world. reachable w -> inv w *)
end