forked from wenhuizhang/summer-school-2020
-
Notifications
You must be signed in to change notification settings - Fork 0
/
exercise01.dfy
73 lines (62 loc) · 2.12 KB
/
exercise01.dfy
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
//#title Coke Machine
//#desc The first state machine specification exercise: fill in actions.
// You are asked to define the state machine for a coke vending machine.
// The machine starts empty and has a maximum capacity of 7 cokes.
// The machine should support the following actions:
// Purchase: dispense one coke from the machine
// Restock: add a number of cokes to the machine
datatype Constants = Constants(capacity:int)
datatype CokeMachine = CokeMachine(numCokes:int)
predicate Init(c:Constants, v:CokeMachine) {
true // Replace me
}
predicate Purchase(c:Constants, v:CokeMachine, v':CokeMachine) {
true // Replace me
}
predicate Restock(c:Constants, v:CokeMachine, v':CokeMachine, numRestock:int)
{
true // Replace me
}
predicate Next(c:Constants, v:CokeMachine, v':CokeMachine) {
|| Purchase(c, v, v')
|| (exists num :: Restock(c, v, v', num))
}
//==========================
// Everything below this line is not part of the specification. It allows
// you to use the verifier to confirm that your state machine has a number
// of desirable properties.
predicate Inv(c:Constants, v:CokeMachine) {
0 <= v.numCokes <= c.capacity
}
lemma SafetyProof()
ensures forall c, v | Init(c, v) :: Inv(c, v)
ensures forall c, v, v' | Inv(c, v) && Next(c, v, v') :: Inv(c, v')
{
forall c, v, v' | Inv(c, v) && Next(c, v, v')
ensures Inv(c, v')
{
if(Purchase(c, v, v')) {
assert Inv(c, v');
} else {
var num :| Restock(c, v, v', num);
assert Inv(c, v');
}
}
}
lemma NonTrivialPurchase()
ensures exists c, v, v' :: Inv(c, v) && Next(c, v, v') && v'.numCokes + 1 == v.numCokes
{
var c := Constants(7);
var v := CokeMachine(1);
var v' := CokeMachine(0);
assert Inv(c, v) && Next(c, v, v') && v'.numCokes + 1 == v.numCokes;
}
lemma NonTrivialRestock()
ensures exists c, v, v' :: Inv(c, v) && Next(c, v, v') && v.numCokes < v'.numCokes
{
var c := Constants(7);
var v := CokeMachine(4);
var v' := CokeMachine(7);
assert Restock(c, v, v', 3);
assert Inv(c, v) && Next(c, v, v') && v.numCokes < v'.numCokes;
}