blob: ff5152d0c34d8c4ddaae90069a42e4dc18c16d6d (
plain)
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
|
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) where T : class {
Contract.Assert(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 && 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) where T : class {
return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
}
[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;
}
}
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) {
}
}
|
