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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
class C {
method M(y: int) returns (x: int)
{
x := 6;
}
var abc: bool;
var xyz: bool;
function method F<A,B,C>(x: int, y: A, z: set<C>, b: bool): B
function G(): int // uninterpreted for now
function H(): int // uninterpreted for now
method BodyLess(y: bool, k: seq<set<object>>) returns (x: int)
method FullBodied(x: int) returns (y: bool, k: seq<set<object>>)
{
}
}
}
module B refines A {
class C {
var k: int;
method M(y: int) returns (x: int)
requires 0 <= y; // error: cannot add a precondition
modifies this; // error: cannot add a modifies clause
ensures 0 <= x; // fine
predicate abc() // error: cannot replace a field with a predicate
var xyz: bool; // error: ...or even with another field
function F // error: cannot replace a "function method" with a "function"
<C,A,B> // error: different list of type parameters
(x: int, y: A, z: seq<C>, // error: different type of parameter z
k: bool) // error: different parameter name
: B
function G(): int
{ 12 } // allowed to add a body
method BodyLess(y: bool, k: seq<set<object>>) returns (x: int)
{ // yes, can give it a body
}
method FullBodied(x: int) returns (y: bool, k: seq<set<object>>)
{
}
}
}
module BB refines B {
class C {
function method G(): int // error: allowed to make a function into a function method
function method H(): int // ...unless this is where the function body is given
{ 10 }
}
}
module Forall0 {
class C {
var a: int
method M()
modifies this
{
}
lemma Lemma(x: int)
{
}
}
}
module Forall1 refines Forall0 {
class C {
var b: int
method M...
{
forall x { Lemma(x); } // allowed
var s := {4};
forall x | x in s ensures x == 4 { } // allowed
forall x { // allowed
calc {
x in s;
==
x == 4;
}
}
forall c | c in {this} {
c.b := 17; // allowed
}
forall c | c in {this} {
c.a := 17; // error: not allowed to update previously defined field
}
}
}
}
|
