diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
| commit | 8911e5c95d4715c2e2626aef67f19793d6f43201 (patch) | |
| tree | d703bfd931802e780430e32f1339cf77adc342a4 /Source/Dafny/cce.cs | |
| parent | 1c375d1889e628fcd2a1a0fc041673a5f4230d84 (diff) | |
Put all sources under \Source directory
Diffstat (limited to 'Source/Dafny/cce.cs')
| -rw-r--r-- | Source/Dafny/cce.cs | 112 |
1 files changed, 112 insertions, 0 deletions
diff --git a/Source/Dafny/cce.cs b/Source/Dafny/cce.cs new file mode 100644 index 00000000..ff5152d0 --- /dev/null +++ b/Source/Dafny/cce.cs @@ -0,0 +1,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) {
+ }
+}
\ No newline at end of file |