seng2011/1/ex4.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

method Eval(x:int) returns (r:int)
requires x > 0;
ensures r == x * x;
{
    var y:int := x;
    var z:int := 0;
    while (y >0)
        decreases y
        invariant (y >= 0 && y <= x && z == x * (x - y));
    {
        z := z + x;
        y := y - 1;
    }
    return z;
}