blob: b1407f10a38d04ff7af738077f9289a2c72164e3 (
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module Cycle {
type MySynonym = MyNewType // error: a cycle
newtype MyNewType = MyIntegerType_WellSupposedly
type MyIntegerType_WellSupposedly = MySynonym
}
module MustBeNumeric {
datatype List<T> = Nil | Cons(T, List)
newtype NewDatatype = List<int> // error: base type must be numeric based
}
module Goodies {
newtype int32 = int
newtype posReal = real
newtype int8 = int32
method M()
{
var k8 := new int8[100];
var s: set<int32>;
var x: posReal;
var y: posReal;
var z: int32;
x := 5.3;
z := 12;
s := {};
s := {40,20};
x := x + y;
var r0 := real(x);
var r1: real := 2.0 * r0;
var i0 := int(z);
var i1: nat := 2 * i0;
assert i1 == 24;
assert r1 == 10.6;
if x == r0 { // error: cannot compare posReal and real
} else if real(x) == r0 {
} else if i0 == int(x) {
} else if i0 == int(real(x)) {
} else if real(i0) == real(x) {
}
if z == i0 { // error: cannot compare int32 and int
} else if int(z) == i0 {
} else if r0 == real(z) {
} else if r0 == real(int(z)) {
} else if int(r0) == int(z) {
}
assert x == z; // error: cannot compare posReal and int32
assert x <= z; // error: cannot compare posReal and int32
assert z < i0; // error: cannot compare int32 and int
assert x > r1; // error: cannot compare posReal and real
var di := z % 2 - z / 2 + if z == 0 then 3 else 100 / z + 100 % z;
var dr := x / 2.0 + if x == 0.0 then 3.0 else 100.0 / x;
dr := dr % 3.0 + 3.0 % dr; // error: mod not supported for real-based types
z, x := di, dr;
var sq := [23, 50];
assert forall ii :: 0 <= ii < |sq| ==> sq[ii] == sq[ii];
var ms := multiset{23.0, 50.0};
assert forall rr :: 0.0 <= rr < 100.0 ==> ms[rr] == ms[rr];
var truncated := r0.Trunc + x.Trunc;
var rounded := (r0 + 0.5).Trunc;
}
}
module Constraints {
newtype SmallInt = x: int where 0 <= x < 100
newtype LargeInt = y: int where 0 <= y < 100
newtype BadConstraint = a: SmallInt
where a + a // error: not a boolean
newtype WotsDisVariable = u :BadConstraint
where u + a < 50 // error: undeclared identifier 'a'
newtype A = x: int where 0 <= x
newtype B = x: A where x < 100
newtype C = B // the constraints 0 <= x < 100 still apply
static predicate IsEven(x: int) // note that this is a ghost predicate
{
x % 2 == 0
}
newtype G = x: int where IsEven(x) // it's okay to use ghost constructs in type constraints
newtype N = nat
newtype OldState = y: real where old(y) == y // error: old is not allowed in constraint
newtype AssertType = s: int where
var k := s;
assert k == s;
k < 10 || 10 <= s
method BadTypeArgs(n: N<int>) // error: N takes no type arguments
}
module CyclicDependencies {
newtype Cycle = x: int where (BadLemma(); false) // error: cycle
static lemma BadLemma()
ensures false;
{
var c: Cycle;
}
}
module SelfCycleTest {
newtype SelfCycle = x: int where var s: SelfCycle := 4; s < 10 // error: cyclic dependency on itself
}
module Module0 {
import Module1
method M(x: int) returns (n: Module1.N9) {
var x := Module1.N9; // error
}
}
module Module1 {
newtype N9 = int
}
|
