From ff05bb6936d433e7be5ded41233214c0517dc2d2 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 19:13:56 -0700 Subject: Make `old` a special case for trigger generation. Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information. --- .../looping-is-hard-to-decide-modulo-equality.dfy | 32 ++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy (limited to 'Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy') diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy new file mode 100644 index 00000000..c54089f2 --- /dev/null +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy @@ -0,0 +1,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) { + 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) { + assert forall c | c in sc :: true || f(c) == old(f(f(c))); +} -- cgit v1.2.3