blob: 0aad9018479dd919eed2c1422891f5ca1e20dc6c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file checks that function applications yield trigger candidates
method M(P: (int -> int) -> bool, g: int -> int)
requires P.requires(g)
requires P(g) {
assume forall f: int -> int :: P.requires(f);
assume forall f: int -> int :: P(f) ==> f.requires(10) && f(10) == 0;
assert forall f: int -> int ::
(forall x :: f.requires(x) && g.requires(x) ==> f(x) == g(x)) ==>
f.requires(10) ==>
f(10) == 0;
}
|