blob: 4e95a452139b8667b05a9890a465ac70671f3bb7 (
plain)
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
|
// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module J0 {
function F0(): int
protected function F1(): int
predicate R0()
protected predicate R1()
}
module J1 refines J0 {
protected function F0(): int // error: cannot add 'protected' modifier
function F1(): int // error: cannot drop 'protected' modifier
protected predicate R0() // error: cannot add 'protected' modifier
predicate R1() // error: cannot drop 'protected' modifier
}
module M0 {
function F(): int { 5 }
protected function G(): int { 5 }
predicate P() { true }
protected predicate Q() { true }
}
module M1 refines M0 {
function F... { 7 } // error: not allowed to change body
protected function G... { 7 } // error: not allowed to change body
predicate P... { true } // error: not allowed to extend body
protected predicate Q... { true } // fine
}
module Y0 {
protected function {:opaque} F(): int { 5 } // error: protected and opaque are incompatible
}
|
