blob: c54089f2d0276ae25eda6c629ee64d4ec1df15ca (
plain)
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
31
32
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file shows cases where loops could hide behind equalities. In all three
// cases we behave the same; that is, we don't warn for loops that would only
// exist in the presence of an equality. The easiest way to understand the
// issue, I (CPC) feel, is to look at the old case: f(x) could very well loop
// with old(f(f(x))) if f(f(x)) did not change the heap at all.
// This equality issue is generally undecidable. It could make sense to special
// case `old`, but KRML and CPC decided against it on 2015-08-21. Future
// experiences could cause a change of mind.
class C { }
function f(c: C): C
function g(c: C): C
function h(c: C, i: int): C
// With explicit arguments
method M0(i: int, j: int, sc: set<C>) {
assert forall c | c in sc :: true || h(c, i) == h(h(c, j), j);
}
// With implicit arguments (f and g respectively, to Apply)
method M1(f: int -> int, g: int -> int) {
assert forall x :: true || f(x) == g(f(x));
}
// With implicit arguments (the heap, to old)
method M2(sc: set<C>) {
assert forall c | c in sc :: true || f(c) == old(f(f(c)));
}
|
