From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Graph/cce.cs | 384 ++++++++++++++++++++++++++-------------------------- 1 file changed, 192 insertions(+), 192 deletions(-) (limited to 'Source/Graph/cce.cs') diff --git a/Source/Graph/cce.cs b/Source/Graph/cce.cs index ef594484..1e0b12a5 100644 --- a/Source/Graph/cce.cs +++ b/Source/Graph/cce.cs @@ -1,193 +1,193 @@ -using System; -using SA=System.Attribute; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Text; -//using Microsoft.Boogie; - -/// -/// A class containing static methods to extend the functionality of Code Contracts -/// - -public static class cce { - //[Pure] - //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); - //} - [Pure] - public static T NonNull(T t) { - Contract.Assert(t != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullElements(IDictionary 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); - //} - /// - /// For possibly-null lists of non-null elements - /// - /// - /// - /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! - /// - [Pure] - public static bool NonNullElements(IEnumerable collection, bool nullability) { - 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(KeyValuePair kvp) { - return kvp.Key != null && kvp.Value != null; - } - [Pure] - public static bool NonNullElements(IEnumerator iEnumerator) { - return iEnumerator != null; - } - //[Pure] - //public static bool NonNullElements(Graphing.Graph 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 toList(PureCollections.Sequence s) { - // List toRet = new List(); - // 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 { +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary 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); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + 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(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph 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 toList(PureCollections.Sequence s) { + // List toRet = new List(); + // 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 { } \ No newline at end of file -- cgit v1.2.3