blob: 3d3839edfa4c6698a4583624747017fdd2248392 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function I(f:int->bool):int->bool
ensures I(f) == f;
predicate G<S>(s:S)
type D<X>
type E
lemma L1<S>(b:int->S)
requires forall i :: b.reads(i) == {};
requires forall i :: b.requires(i);
requires I(j => G(b(j)))(0); // PRECONDITION NOT SATISFIED BY L2
lemma L2(b:int->D<E>)
requires forall i :: b.reads(i) == {};
requires forall i :: b.requires(i);
requires I(j => G(b(j)))(0);
{
L1(b); // FAILS TO SATISFY L1's PRECONDITION
}
|