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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
using System;
using SA=System.Attribute;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Text;
//using Microsoft.Boogie;
/// <summary>
/// A class containing static methods to extend the functionality of Code Contracts
/// </summary>
public static class cce {
//[Pure]
//public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
// return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
//}
[Pure]
public static T NonNull<T>(T t) where T : class {
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<T>() != null);
return t;
}
[Pure]
public static bool NonNullElements<T>(IEnumerable<T> collection) where T : class {
return collection != null && Contract.ForAll(collection, c => c != null);
}
[Pure]
public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class {
return collection != null && cce.NonNullElements(collection.Values);
}
//[Pure]
//public static bool NonNullElements(VariableSeq collection) {
// return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
//}
/// <summary>
/// For possibly-null lists of non-null elements
/// </summary>
/// <typeparam name="T"></typeparam>
/// <param name="collection"></param>
/// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param>
/// <returns></returns>
[Pure]
public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) where T : class {
return (nullability && collection == null) || cce.NonNullElements(collection);
//Should be the same as:
/*if(nullability&&collection==null)
* return true;
* return cce.NonNullElements(collection)
*/
}
[Pure]
public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) where TKey : class where TValue : class {
return kvp.Key != null && kvp.Value != null;
}
[Pure]
public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) where T : class {
return iEnumerator != null;
}
[Pure]
public static bool NonNull<T>(HashSet<T> set) where T : class {
return set != null && !set.Contains(null);
}
//[Pure]
//public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
// return cce.NonNullElements(graph.TopologicalSort());
//}
[Pure]
public static void BeginExpose(object o) {
}
[Pure]
public static void EndExpose() {
}
[Pure]
public static bool IsPeerConsistent(object o) {
return true;
}
[Pure]
public static bool IsConsistent(object o) {
return true;
}
[Pure]
public static bool IsExposable(object o) {
return true;
}
[Pure]
public static bool IsExposed(object o) {
return true;
}
[Pure]
public static bool IsNew(object o) {
return true;
}
public static class Owner {
[Pure]
public static bool Same(object o, object p) {
return true;
}
[Pure]
public static void AssignSame(object o, object p) {
}
[Pure]
public static object ElementProxy(object o) {
return o;
}
[Pure]
public static bool None(object o) {
return true;
}
[Pure]
public static bool Different(object o, object p) {
return true;
}
[Pure]
public static bool New(object o) {
return true;
}
}
[Pure]
public static void LoopInvariant(bool p) {
Contract.Assert(p);
}
public class UnreachableException : Exception {
public UnreachableException() {
}
}
//[Pure]
//public static bool IsValid(Microsoft.Dafny.Expression expression) {
// return true;
//}
//public static List<T> toList<T>(PureCollections.Sequence s) {
// List<T> toRet = new List<T>();
// foreach (T t in s.elems)
// if(t!=null)
// toRet.Add(t);
// return toRet;
//}
//internal static bool NonNullElements(Set set) {
// return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
//}
}
public class PeerAttribute : SA {
}
public class RepAttribute : SA {
}
public class CapturedAttribute : SA {
}
public class NotDelayedAttribute : SA {
}
public class NoDefaultContractAttribute : SA {
}
public class VerifyAttribute : SA {
public VerifyAttribute(bool b) {
}
}
public class StrictReadonlyAttribute : SA {
}
public class AdditiveAttribute : SA {
}
public class ReadsAttribute : SA {
public enum Reads {
Nothing,
Everything,
};
public ReadsAttribute(object o) {
}
}
public class GlobalAccessAttribute : SA {
public GlobalAccessAttribute(bool b) {
}
}
public class EscapesAttribute : SA {
public EscapesAttribute(bool b, bool b_2) {
}
}
public class NeedsContractsAttribute : SA {
public NeedsContractsAttribute() {
}
public NeedsContractsAttribute(bool ret, bool parameters) {
}
public NeedsContractsAttribute(bool ret, int[] parameters) {
}
}
public class ImmutableAttribute : SA {
}
public class InsideAttribute : SA {
}
public class SpecPublicAttribute : SA {
}
public class ElementsPeerAttribute : SA {
}
public class ResultNotNewlyAllocatedAttribute : SA {
}
public class OnceAttribute : SA {
}
|
