35 lines
955 B
Plaintext
35 lines
955 B
Plaintext
function More(x: int): int {
|
|
if x <= 0 then 1 else More(x - 2) + 3
|
|
}
|
|
|
|
lemma {:induction false} Increasing(x: int)
|
|
decreases x
|
|
ensures x < More(x)
|
|
{ // 0:
|
|
// x is an int, x can be any value.
|
|
if x <= 0 { // 1: x <= 0 Therefore More(x) == 1 => x <= 0 < 1 == More(x) => x < More(x)
|
|
} else { // 2: Work back to basecase, x > 0 ==> repeated x - 2 eventually enters basecase.
|
|
Increasing(x-2);
|
|
}
|
|
}
|
|
|
|
method ExampleLemmaUse(a: int) {
|
|
// var b := More(a);
|
|
// Increasing(a);
|
|
// Increasing(b);
|
|
// var c := More(b);
|
|
// assert 2 <= c - a;
|
|
|
|
Increasing(a); // this call is along all control paths
|
|
var b := More(a);
|
|
Increasing(b);
|
|
b := More(b);
|
|
// Increasing(b);
|
|
// if a < 1000 {
|
|
// Increasing(More(a)); // we learn More(a) < More(More(a))
|
|
// // only here, i.e., when a < 1000
|
|
// assert 2 <= b - a; // this verifies
|
|
// }
|
|
assert 2 <= b - a; // this does not verify
|
|
}
|