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
|
using System;
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 T NonNull<T>(T t) {
Contract.Assert(t != null);
return t;
}
[Pure]
public static bool NonNullElements<T>(IEnumerable<T> collection) {
return collection != null && Contract.ForAll(collection, c => c != null);
}
[Pure]
public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
}
[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) {
// return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
//}
[Pure]
public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
return kvp.Key != null && kvp.Value != null;
}
[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;
}
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 void LoopInvariant(bool p) {
Contract.Assert(p);
}
public class UnreachableException : Exception {
public UnreachableException() {
}
}
//[Pure]
//public static bool IsValid(Microsoft.Dafny.Expression expression) {
// return true;
//}
internal static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
return iEnumerator != null;
}
}
public class PeerAttribute : System.Attribute {
}
public class RepAttribute : System.Attribute {
}
public class CapturedAttribute : System.Attribute {
}
public class NotDelayedAttribute : System.Attribute {
}
public class NoDefaultContractAttribute : System.Attribute {
}
public class VerifyAttribute : System.Attribute {
public VerifyAttribute(bool b) {
}
}
public class StrictReadonlyAttribute : System.Attribute {
}
public class AdditiveAttribute : System.Attribute {
}
public class ReadsAttribute : System.Attribute {
public enum Reads {
Nothing,
};
public ReadsAttribute(object o) {
}
}
public class GlobalAccessAttribute : System.Attribute {
public GlobalAccessAttribute(bool b) {
}
}
public class EscapesAttribute : System.Attribute {
public EscapesAttribute(bool b, bool b_2) {
}
}
|
