blob: 1b1923c3a7abdd08fb9022044de085b21a2b4c38 (
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
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
|
module TestModule {
copredicate P(b: bool)
{
!b && Q(null)
}
copredicate Q(a: array<int>)
{
a == null && P(true)
}
copredicate S(d: set<int>)
{
this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
this.S#[5](d) &&
S#[5](d) &&
S#[_k](d) // error: _k is not an identifier in scope
}
comethod CM(d: set<int>)
{
var b;
b := this.S#[5](d);
b := S#[5](d);
this.CM#[5](d);
CM#[5](d);
}
}
module GhostCheck0 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
method UseStream0(s: Stream)
{
var x := 3;
if (s == s.tail) { // error: this operation is allowed only in ghost contexts
x := x + 2;
}
}
}
module GhostCheck1 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
method UseStream1(s: Stream)
{
var x := 3;
if (s ==#[20] s.tail) { // this seems innocent enough, but it's currently not supported by the compiler, so...
x := x + 7; // error: therefore, this is an error
}
}
}
module GhostCheck2 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
ghost method UseStreamGhost(s: Stream)
{
var x := 3;
if (s == s.tail) { // fine
x := x + 2;
}
}
}
module Mojul0 {
copredicate D()
reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
{
true
}
copredicate NoEnsuresPlease(m: nat)
ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
{
m < 75
}
// Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
}
module Mojul1 {
copredicate A() { B() } // error: SCC of a copredicate must include only copredicates
predicate B() { A() }
copredicate X() { Y() }
copredicate Y() { X#[10]() } // error: X is not allowed to depend on X#
comethod M()
{
N();
}
comethod N()
{
Z();
W(); // error: not allowed to make co-recursive call to non-comethod
}
ghost method Z() { }
ghost method W() { M(); }
comethod G() { H(); }
comethod H() { G#[10](); } // fine for comethod/prefix-method
}
|
