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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function f(x: int, y: int): int
lemma Associativity(x: int, y: int, z: int)
ensures f(x, f(y, z)) == f(f(x, y), z);
lemma Monotonicity(y: int, z: int)
requires y <= z;
ensures forall x :: f(x, y) <= f(x, z);
lemma DiagonalIdentity(x: int)
ensures f(x, x) == x;
method M(a: int, b: int, c: int, x: int)
requires c <= x == f(a, b);
{
calc {
f(a, f(b, c));
{ Associativity(a, b, c); }
f(f(a, b), c);
{ assert f(a, b) == x; }
f(x, c);
<= { assert c <= x; Monotonicity(c, x); }
f(x, x);
{ DiagonalIdentity(x); }
x;
}
}
|
