diff options
| author |  mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
| commit | a42f800cad7918d42349914a4b8f0d58d95d6531 (patch) | |
| tree | e3f84afafefa83a5add6fd34299e29801a832b6f /Dafny/cce.cs | |
| parent | b9f45ea020cab2f5ce7de69a60dc6a19f7df810e (diff) | |
Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
Diffstat (limited to 'Dafny/cce.cs')
| -rw-r--r-- | Dafny/cce.cs | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Dafny/cce.cs b/Dafny/cce.cs index 8391361b..ff5152d0 100644 --- a/Dafny/cce.cs +++ b/Dafny/cce.cs @@ -10,24 +10,24 @@ using Microsoft.Boogie; public static class cce {
[Pure]
- public static T NonNull<T>(T t) {
+ public static T NonNull<T>(T t) where T : class {
Contract.Assert(t != null);
return t;
}
[Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
+ public static bool NonNullElements<T>(IEnumerable<T> collection) where T : class {
return collection != null && Contract.ForAll(collection, c => c != null);
}
[Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values);
+ public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class {
+ return collection != null && NonNullElements(collection.Values);
}
[Pure]
public static bool NonNullElements(VariableSeq collection) {
return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
}
[Pure]
- public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
+ public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) where T : class {
return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
}
[Pure]
|