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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class MyClass<T> {
var f: T;
}
method M<T>()
{
var a, b := new T[100], new T[100];
forall i | 0 <= i < 100 {
a[3] := *; // RHS is * -- this is okay
}
forall i | 0 <= i < 100 {
a[0] := b[0]; // RHSs are the same -- this is okay
}
forall i | 0 <= i < 100 {
a[0] := b[i]; // error: LHS's may be the same (while RHSs are different)
}
}
method N<T>(a: MyClass<T>, b: MyClass<T>)
requires a != null && b != null;
modifies a, b;
{
var q := [a, b];
forall i | 0 <= i < 2 {
q[0].f := *; // RHS is * -- this is okay
}
forall i | 0 <= i < 2 {
q[0].f := q[0].f; // RHSs are the same -- this is okay
}
forall i | 0 <= i < 2 {
q[0].f := q[i].f; // error: LHS's may be the same (while RHSs are different)
}
}
method P<T>(t0: T, t1: T, t2: T) {
var a: T, b: T;
a, a, a := *, t0, *; // only one non-* RHS per variable -- this is okay
a, a, b, a, b := *, t1, t2, *, *; // only one non-* RHS per variable -- this is okay
a, a, b, a, b := *, t1, t2, t0, *; // error: duplicate LHS -- t0 and t1 may be different
}
method Q<T>(c0: MyClass<T>, c1: MyClass<T>)
requires c0 != null && c1 != null;
modifies c0, c1;
{
c0.f, c1.f := c0.f, c0.f; // okay -- RHSs are the same
c0.f, c0.f, c0.f, c0.f := *, *, c1.f, *; // okay -- only one RHS is non-*
c0.f, c0.f, c0.f, c0.f := c0.f, *, c1.f, *; // error -- duplicate LHR
}
method R<T>(i: nat, j: nat)
requires i < 10 && j < 10;
{
var a := new T[10];
a[i], a[j] := a[5], a[5]; // okay -- RHSs are the same
a[i], a[i], a[i], a[i] := *, *, a[5], *; // okay -- only one RHS is non-*
a[i], a[i], a[i], a[j] := *, a[i], a[j], a[i]; // error -- possible duplicate LHS
}
method S<T>(i: nat, j: nat)
requires i < 10 && j < 20;
{
var a := new T[10,20];
a[i,j], a[i,i] := a[5,7], a[5,7]; // okay -- RHSs are the same
a[i,j], a[i,j], a[i,j], a[i,j] := *, *, a[5,7], *; // okay -- only one RHS is non-*
a[i,j], a[i,j], a[i,j], a[i,i] := *, a[i,i], a[i,j], a[i,i]; // error -- possible duplicate LHS
}
|
