Here some examples a briefly discussed. We present the necessary templates and the resulting invariants that we generated using Prinsys. The full analysis including the computation of expted values is omitted here because this is not the focus of our work and can be done rather easily once the invariant is found.
This example is discussed in a paper that is currently under review...
Duelling Cowboys. [McIver, Morgan: Abstraction, Refinement and Proof for Probabilistic Systems, 2004]
The pGCL program in List. 1 models the following situation: There are two cowboys, A and B, who are fighting a duel. They take
turns, shooting at each other until one of them is hit. If A (resp. B) shoots then
he hits B (resp. A) with probability a (resp. b) where a, b ≠ 0. Note, it is a
distinct feature that we do not have to specify exact probabilities and instead
reason over arbitrary parameters a and b. We are interested in the probability
that cowboy A wins the duel, i.e. wlp(prog,[turn = 0]).
We look for an expectation T that satisfies T ≤ [turn = 0] upon termination of
the loop. Observe that on entering the loop, we have continue = 1 and either
turn = 0 or turn = 1. With these insights we formulate the template
turn := 0; // turn = 0 (1) means cowboy A (B) is shooting
continue := 1;
while ( continue - 1 = 0) {
if (turn = 0) {
(continue := 0 [ a ] turn := 1);
} else {
(continue := 0 [ b ] turn := 0);
}
}
T = [turn = 0 and continue = 0] * (1) + [turn = 0 and continue - 1 = 0] * (α) + [turn-1 = 0 and continue-1 = 0] * (β) (1)
The parameter α is the probability that it is A's turn and he wins, β is the
probability that it is B's turn and A wins the duel. Note that initially, turn =
0 and continue = 1 holds and thus α will be the probability that cowboy A wins
the contest. We feed this program and template into our tool and it generates
the following solution to the consecution condition:
a*β - a + α - β ≤ 0 and b*α - α + β ≤ 0 (2)
We have to ensure that the generated invariant induces
a sound annotation. In this case we rely on the fact that α and β are probabilities and thus T lies between 0 and 1. From (2) we deduce β ≤ (1 - b)α and
α ≤ a/(a+b-ab). Since we are interested in the maximal probability that we can
guarantee, we choose the greatest values permitted by these inequalities. This
gives us an instance I of the template T from (1)
I = [turn = 0 and continue = 0] * (1) + [turn = 0 and continue - 1 = 0] * (a/(a + b - ab))
+ [turn - 1 = 0 and continue - 1 = 0] * (((1 - b)a)/(a + b - ab))
It follows that cowboy A wins the duel with probability a/(a+b-ab).
Biased Coin. [Hurd: Formal Verification of Probabilistic Algorithms, 2002.]
This program simulates a "biased" coin flip by repeatedly flipping a fair
coin.
x := p;
b := true;
while (b - 1 = 0) {
(b := false [0.5] b := true);
if (b - 1 = 0) {
x:= 2*x;
if (x - 1 >= 0) {
x:= x-1;
} else {
skip;
}
}
else if (x - 0.5 >= 0) {
x:= 1;
}
else {
x:= 0;
}
}
Our is aim is to prove that the probability of the outcome "x = 1" is p. Therefore we need an invariant
that will ensure x = 1 after the loop and which has a worth of p at initialisation. It is plain to see
that the loop can only terminate if b = 0 but in that case the variable x is set to
either zero or one in the loop body. Testing our hypothesis
T = [b - 1 = 0 or x = 0 or x - 1 = 0)] * (1)
with the tool we learn that our observation is correct. We see that this annotation simplifies to
[x = 0] * (1) + [x - 1 = 0] * (1)
after termination of the loop because then surely the guard of the while-loop does not hold
any more. Now we need to express the weight in terms of x such that T implies [x - 1 = 0] * (1) upon termination
and wlp(x := p; b := true; T) = p. Hence we choose
T = [b - 1 = 0 or x = 0 or x - 1 = 0)] * (x)
and see whether our tool will return true for all constraints. Apparently this is not the case. This
is because we only know that if the guard is false, then x is either zero or one but otherwise we do
not anything about x. So the consecution condition is satisfied but the boundedness conditions
are both violated.
Let us start anew and try to discover an invariant which limits the range of x. Use
T = [x - a ≤ 0] * (1)
to find out that x is invariantly between zero and one. This qualitative invariant we can insert
into the previous one and obtain
T = [x ≥ 0 and x - 1 ≤ 0 and (b - 1 = 0 or x = 0 or x - 1 = 0))] * (1)
Now Prinsys reports that all conditions are met and we can successfully carry out the proof
that Pr(x = 1) = p.
Binomial Distribution. [Katoen, McIver, Meinicke, Morgan: Linear-Invariant Generation for Probabilistic Programs, 2011]
The following program samples a value x according to the binomial distribution. We want to show that indeed the expected value of x is M*p.
x := 0;
n := 0;
while (n - M + 1 <= 0) {
(x := x + 1 [p] skip);
n := n + 1;
}
We approach our goal iteratively. First, we start with a qualitative template
which might help us to limit a variable's range.
In our qualitative template we express that variable x is invariantly non-negative. The same holds for n. In particular, x is always at most n.
Finally, an upper bound for n is given by the guard. So the template becomes:
T = [x ≥ 0 and x-n ≤ 0 and n-M ≤ 0]*(1)
We enter the hypothetical invariant directly into our tool and since there are no
parameters the resulting constraints can only be true or false. In this case the result is true.
So far we have a standard invariant that establishes a relation between variables and imposes
lower and upper bounds on them. After the discovery of a qualitative invariant, we can proceed and reason about its weight, thereby making
it lesser. McIver and Morgan call this approach "modular reasoning".
Let us consider the template
T = [x ≥ 0 and x - n ≤ 0 and n - M ≤ 0] * (a*x + b*n + c)
Prinsys provides a hint for further refinement of this template.
The generated constraint for the consecution condition is
a*p + b ≥ 0 or M - 1 < 0
Remember that M is the number of loop iterations. Thus M is certainly greater than one. Therefore
the first inequality must hold. Assume b = -a*p. This simplifies the template to
T = [x ≥ 0 and x - n ≤ 0 and n - M ≤ 0] * (a*x - a*p*n + c)
Running Prinsys once again shows that the consecution condition is satisfied
and now we only have to bound (a*x - a*p*n + c) between zero and one. In order to
find useful a and c we consider the values of x and n before the first iteration of the while-loop
and after termination. This brings us to
a = 1/M and consequently c = p.
Thereby we scale x and n down to [0,...,1] and make sure that by the end of the program x/M
remains while the rest of the term cancels.
Prinsys confirms this choice because it reduces the given template
T = [x ≥ 0 and x - n ≤ 0 and n - M ≤ 0] * ((1/M)*x - (p/M)*n + p)
to true.
30 Apr. 2012