Test/dafny0/Superposition.dfy


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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

// RUN: %dafny /compile:0 /tracePOs /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

module M0 {
  class C {
    method M(c: C, x: int, y: int) returns (r: int)
      requires 0 <= x && 0 <= y;
      ensures r < 100;
    {
      if (c == null) {
        assert c == null;
      } else if (*) {
        assert 0 <= x;
      } else {
        assert 0 <= y;
      }
      r := 8;
    }

    protected predicate P(x: int)
      ensures true;  // this postcondition will not be re-checked in refinements, because it does not mention P itself (or anything else that may change in the refinement)
      ensures x < 60 ==> P(x);
    {
      true
    }

    predicate Q(x: int)
      ensures Q(x) ==> x < 60;  // error: postcondition violation
    {
      true
    }

    predicate R(x: int)
      ensures R(x) ==> x < 60;  // error: postcondition violation
    {
      true
    }
  }
}

module M1 refines M0 {
  class C {
    method M...  // no further proof obligations for M, which is just making M0.M more deterministic
    {
      if ... {}
      else if (x == y) {}
      else {}
    }

    protected predicate P...  // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()
    {
      false  // with this strengthening of P(), the postcondition fails (still, note that only one of the postconditions is re-checked)
    }

    predicate Q...  // we don't want another error about Q's body here (because it should not be re-checked here)
    // Ditto for R
  }
}