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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This identity function is used to so that if the occurrence of i below
// that is enclosed by Id gets chosen by the SMT solver as a trigger, then
// Id will be part of that trigger. This means that the quantifier will
// not match, and thus the 'forall' statement will be useless and the method
// will not verify. If, however, the inverting functionality in Dafny
// works properly, then the 'i' in the right-hand side of the forall assignments
// below will not be chosen in any trigger, and then the methods should
// verify.
function method Id(x: int): int { x }
method Copy<T>(a: array<T>) returns (r: array<T>)
requires a != null;
ensures fresh(r) && r.Length == a.Length && forall k :: 0 <= k < a.Length ==> r[k] == a[k];
{
r := new T[a.Length];
forall i | 0 <= i < a.Length {
r[i] := a[Id(i)];
}
}
method ShiftLeftA<T>(a: array<T>, n: nat) returns (r: array<T>)
requires a != null && n <= a.Length;
ensures fresh(r) && r.Length == a.Length - n && forall k :: n <= k < a.Length ==> r[k - n] == a[k];
{
r := new T[a.Length - n];
forall i | 0 <= i < a.Length - n {
r[i] := a[i + n];
}
}
method ShiftLeftB<T>(a: array<T>, n: nat) returns (r: array<T>)
requires a != null && n <= a.Length;
ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
{
r := new T[a.Length - n];
forall i | n <= i < a.Length {
r[i - n] := a[Id(i)];
}
}
method ShiftLeftC<T>(a: array<T>, n: nat) returns (r: array<T>)
requires a != null && n <= a.Length;
ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
{
r := new T[a.Length - n];
forall i | n <= i < a.Length {
r[i + 15 - n - 15] := a[Id(i)];
}
}
method Insert<T>(a: array<T>, p: nat, n: nat) returns (r: array<T>)
requires a != null && p <= a.Length;
ensures fresh(r) && r.Length == a.Length + n;
ensures forall k :: 0 <= k < p ==> r[k] == a[k];
ensures forall k :: p <= k < a.Length ==> r[k + n] == a[k];
{
r := new T[a.Length + n];
forall i | 0 <= i < a.Length {
r[if i < p then i else i + n] := a[Id(i)];
}
}
method RotateA<T>(a: array<T>) returns (r: array<T>)
requires a != null;
ensures fresh(r) && r.Length == a.Length;
ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
{
r := new T[a.Length];
forall i | 0 <= i < a.Length {
r[(i + 1) % a.Length] := a[Id(i)]; // error: Dafny does not find an inverse for this one,
// which causes Z3 to pick Id(i) as the trigger, which
// causes the verification to fail.
}
}
method RotateB<T>(a: array<T>) returns (r: array<T>)
requires a != null;
ensures fresh(r) && r.Length == a.Length;
ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
{
r := new T[a.Length];
forall i | 0 <= i < a.Length {
r[if i + 1 == a.Length then 0 else i + 1] := a[Id(i)]; // error: Dafny does not find an inverse
// for this one, so (like in RotateA),
// the verification fails.
}
}
method RotateC<T>(a: array<T>) returns (r: array<T>)
requires a != null;
ensures fresh(r) && r.Length == a.Length;
ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
{
r := new T[a.Length];
forall i | 0 <= i < a.Length {
r[if i == a.Length - 1 then 0 else i + 1] := a[Id(i)]; // yes, Dafny can invert this one
}
}
method RotateD<T>(a: array<T>) returns (r: array<T>)
requires a != null;
ensures fresh(r) && r.Length == a.Length;
ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
{
r := new T[a.Length];
forall i | 0 <= i < a.Length {
r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)]; // yes, Dafny can invert this one
}
}
// autoTriggers added because it causes a slight rephrasing of an error
// message.
|
