dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1180b.dfy at master · Dargones/dafny · GitHub

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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
// RUN: %exits-with 4 %verify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// verification errors

module StartingFromOpaqueType {
  abstract module A {
    type Ty {
      const c: nat
      function F(x: nat): nat
        requires x != 7
        ensures F(x) == c
      method M(x: nat) returns (r: nat)
        requires x != 9
        ensures r == x
    }
    method Caller(t: Ty, x: int) {
      var c := t.c;
      if c != 9 {
        var r := t.M(t.c);
        var u := t.F(2 * c);
        assert r == u;
      }
    }
  }
  module OpaqueType refines A {
    type Ty ... {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
  module Datatype refines A {
    datatype Ty = Make(w: int) {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
  module Codatatype refines A {
    codatatype Ty = Make(w: int) {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
  module Newtype refines A {
    newtype Ty = int {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
  module Class refines A {
    class Ty {
      constructor () {
        c := 65;
      }
      var q: int
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
  module Trait refines A {
    trait Ty extends object {
      var q: int
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
}

module StartingFromDatatype {
  abstract module A {
    datatype Ty = Make(w: int) {
      const c: nat
      function F(x: nat): nat
        requires x != 7
        ensures F(x) == c
      method M(x: nat) returns (r: nat)
        requires x != 9
        ensures r == x
    }
  }
  module Datatype refines A {
    datatype Ty ... {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
}

module StartingFromNewtype {
  abstract module A {
    newtype Ty = int {
      const c: nat
      function F(x: nat): nat
        requires x != 7
        ensures F(x) == c
      method M(x: nat) returns (r: nat)
        requires x != 9
        ensures r == x
    }
  }
  module Newtype refines A {
    newtype Ty ... {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
}

module StartingFromClass {
  abstract module A {
    class Ty {
      const c: nat
      function F(x: nat): nat
        requires x != 7
        ensures F(x) == c
      method M(x: nat) returns (r: nat)
        requires x != 9
        ensures r == x
    }
  }
  module Newtype refines A {
    class Ty ... {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
}

module StartingFromTrait {
  abstract module A {
    trait Ty {
      const c: nat
      function F(x: nat): nat
        requires x != 7
        ensures F(x) == c
      method M(x: nat) returns (r: nat)
        requires x != 9
        ensures r == x
    }
  }
  module Newtype refines A {
    trait Ty ... {
      function F(x: nat): nat { x } // error: postcondition violation
      method M(x: nat) returns (r: nat) { r := c; } // error: postcondition violation
    }
  }
}