Download MONA Version 1.4 User Manual

MONA 1.4
2.7
Example: Reasoning about queues
# Qe describes the valid indices of a queue
pred isWfQueue(var2 Qe) =
all1 p: (p in Qe & p > 0 => p - 1 in Qe);
# isx holds if p
pred is0(var1 p,
pred is1(var1 p,
pred is2(var1 p,
pred is3(var1 p,
contains
var2 Qe,
var2 Qe,
var2 Qe,
var2 Qe,
an x
Q1, Q2)
Q1, Q2)
Q1, Q2)
Q1, Q2)
=
=
=
=
p
p
p
p
in
in
in
in
Qe
Qe
Qe
Qe
# lt compares the elements at positions p
pred lt(var1 p, q, var2 Qe, Q1, Q2) =
(is0(p, Qe, Q1, Q2) & ~is0(q, Qe, Q1,
| (is1(p, Qe, Q1, Q2) & (is2(q, Qe, Q1,
| (is2(p, Qe, Q1, Q2) & (is3(q, Qe, Q1,
&
&
&
&
p
p
p
p
notin
notin
in Q1
in Q1
Q1 & p notin Q2;
Q1 & p in Q2;
& p notin Q2;
& p in Q2;
and q of a queue
Q2))
Q2) | is3(q, Qe, Q1, Q2)))
Q2)));
# isLast holds if p is the last element in the queue
pred isLast(var1 p, var2 Qe) =
p in Qe & (all1 q’: q’ in Qe => q’ <= p);
# an ordered queue of length l
pred Queue(var2 Qe, Q1, Q2, var1 l) =
isLast(l - 1, Qe)
& (all1 p, q: p < q & p in Qe & q in Qe => lt(p, q, Qe, Q1, Q2));
# eqQueue2 compares elements in two queues
pred eqQueue2(var1 p, q, var2 Q1, Q2, Q1’, Q2’) =
(p in Q1 <=> q in Q1’) & (p in Q2 <=> q in Q2’);
# LooseOne holds about a queue Q and a queue Q’ if
# queue Q’ is the same as Q except that one
# element (denoted by p below) is removed
pred LooseOne(var2 Qe, Q1, Q2, Qe’, Q1’, Q2’) =
ex1 p: p in Qe
& (all1 q: (~isLast(q, Qe) => (q in Qe <=> q in Qe’))
& (isLast(q, Qe) => (q notin Qe’)))
& (all1 q: q < p & q in Qe => eqQueue2(q, q, Q1, Q2, Q1’, Q2’))
& (all1 q: q > p & q in Qe => eqQueue2(q, q - 1, Q1, Q2, Q1’, Q2’));
var2 Qe, Q1, Q2;
var2 Qe’, Q1’, Q2’;
# the queue Q
# the queue Q’
assert isWfQueue(Qe);
# the primed variables denote a queue of length 3 containing
# three of the elements 0, 1, 2, 3 in that order and the element 3
Queue(Qe, Q1, Q2, 4);
# the queue Q is a queue of length 3
# containing the elements 0, 1, 2, 3
LooseOne(Qe, Q1, Q2, Qe’, Q1’, Q2’); # Q’ is Q except for one element
ex1 p: is3(p, Qe’, Q1’, Q2’); # Q’ does contain the element 3
Figure 6: lossy queue.mona
17