Contracts.cs source code in C# .NET

Source code for the .NET framework in C#

                        

Code:

/ 4.0 / 4.0 / untmp / DEVDIV_TFS / Dev10 / Releases / RTMRel / ndp / clr / src / BCL / System / Diagnostics / Contracts / Contracts.cs / 1305376 / Contracts.cs

                            // ==++== 
//
//   Copyright (c) Microsoft Corporation.  All rights reserved.
//
// ==--== 
/*============================================================
** 
** Class:  Contract 
**
** [....],mbarnett 
**
** Purpose: The contract class allows for expressing preconditions,
** postconditions, and object invariants about methods in source
** code for runtime checking & static analysis. 
**
** Two classes (Contract and ContractHelper) are split into partial classes 
** in order to share the public front for multiple platforms (this file) 
** while providing separate implementation details for each platform.
** 
===========================================================*/
#define DEBUG // The behavior of this contract library should be consistent regardless of build type.

#if SILVERLIGHT 
#define FEATURE_UNTRUSTED_CALLERS
 
#elif REDHAWK_RUNTIME 

#elif BARTOK_RUNTIME 

#else // CLR
#define FEATURE_UNTRUSTED_CALLERS
#define FEATURE_RELIABILITY_CONTRACTS 
#define FEATURE_SERIALIZATION
#endif 
 
using System;
using System.Collections.Generic; 
using System.Diagnostics.CodeAnalysis;

#if FEATURE_RELIABILITY_CONTRACTS
using System.Runtime.ConstrainedExecution; 
#endif
#if FEATURE_UNTRUSTED_CALLERS 
using System.Security; 
using System.Security.Permissions;
#endif 

namespace System.Diagnostics.Contracts {

    #region Attributes 

    ///  
    /// Methods and classes marked with this attribute can be used within calls to Contract methods. Such methods not make any visible state changes. 
    /// 
    [Conditional("CONTRACTS_FULL")] 
    [AttributeUsage(AttributeTargets.Constructor | AttributeTargets.Method | AttributeTargets.Property | AttributeTargets.Event | AttributeTargets.Delegate | AttributeTargets.Class | AttributeTargets.Parameter, AllowMultiple = false, Inherited = true)]
    public sealed class PureAttribute : Attribute
    {
    } 

    ///  
    /// Types marked with this attribute specify that a separate type contains the contracts for this type. 
    /// 
    [Conditional("CONTRACTS_FULL")] 
    [Conditional("DEBUG")]  // Hack: For createBclSmall, make sure to include contract classes in AMD64DBG builds.
    [AttributeUsage(AttributeTargets.Class | AttributeTargets.Interface | AttributeTargets.Delegate, AllowMultiple = false, Inherited = false)]
    public sealed class ContractClassAttribute : Attribute
    { 
        private Type _typeWithContracts;
 
        public ContractClassAttribute(Type typeContainingContracts) 
        {
            _typeWithContracts = typeContainingContracts; 
        }

        public Type TypeContainingContracts {
            get { return _typeWithContracts; } 
        }
    } 
 
    /// 
    /// Types marked with this attribute specify that they are a contract for the type that is the argument of the constructor. 
    /// 
    [Conditional("CONTRACTS_FULL")]
    [AttributeUsage(AttributeTargets.Class, AllowMultiple = false, Inherited = false)]
    public sealed class ContractClassForAttribute : Attribute 
    {
        private Type _typeIAmAContractFor; 
 
        public ContractClassForAttribute(Type typeContractsAreFor)
        { 
            _typeIAmAContractFor = typeContractsAreFor;
        }

        public Type TypeContractsAreFor { 
            get { return _typeIAmAContractFor; }
        } 
    } 

    ///  
    /// This attribute is used to mark a method as being the invariant
    /// method for a class. The method can have any name, but it must
    /// return "void" and take no parameters. The body of the method
    /// must consist solely of one or more calls to the method 
    /// Contract.Invariant. A suggested name for the method is
    /// "ObjectInvariant". 
    ///  
    [Conditional("CONTRACTS_FULL")]
    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false, Inherited = false)] 
    public sealed class ContractInvariantMethodAttribute : Attribute
    {
    }
 
    /// 
    /// Attribute that specifies that an assembly is a reference assembly with contracts. 
    ///  
    [AttributeUsage(AttributeTargets.Assembly)]
    public sealed class ContractReferenceAssemblyAttribute : Attribute 
    {
    }

    ///  
    /// Methods (and properties) marked with this attribute can be used within calls to Contract methods, but have no runtime behavior associated with them.
    ///  
    [Conditional("CONTRACTS_FULL")] 
    [AttributeUsage(AttributeTargets.Method | AttributeTargets.Property, AllowMultiple = false, Inherited = true)]
    public sealed class ContractRuntimeIgnoredAttribute : Attribute 
    {
    }

    /* 
#if FEATURE_SERIALIZATION
    [Serializable] 
#endif 
    internal enum Mutability
    { 
        Immutable,    // read-only after construction, except for lazy initialization & caches
        // Do we need a "deeply immutable" value?
        Mutable,
        HasInitializationPhase,  // read-only after some point. 
        // Do we need a value for mutable types with read-only wrapper subclasses?
    } 
 
    // Note: This hasn't been thought through in any depth yet.  Consider it experimental.
    // We should replace this with Joe's concepts. 
    [Conditional("CONTRACTS_FULL")]
    [AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct, AllowMultiple = false, Inherited = false)]
    [SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")]
    internal sealed class MutabilityAttribute : Attribute 
    {
        private Mutability _mutabilityMarker; 
 
        public MutabilityAttribute(Mutability mutabilityMarker)
        { 
            _mutabilityMarker = mutabilityMarker;
        }

        public Mutability Mutability { 
            get { return _mutabilityMarker; }
        } 
    } 
    */
 
    /// 
    /// Instructs downstream tools whether to assume the correctness of this assembly, type or member without performing any verification or not.
    /// Can use [ContractVerification(false)] to explicitly mark assembly, type or member as one to *not* have verification performed on it.
    /// Most specific element found (member, type, then assembly) takes precedence. 
    /// (That is useful if downstream tools allow a user to decide which polarity is the default, unmarked case.)
    ///  
    ///  
    /// Apply this attribute to a type to apply to all members of the type, including nested types.
    /// Apply this attribute to an assembly to apply to all types and members of the assembly. 
    /// Apply this attribute to a property to apply to both the getter and setter.
    /// 
    [Conditional("CONTRACTS_FULL")]
    [AttributeUsage(AttributeTargets.Assembly | AttributeTargets.Class | AttributeTargets.Struct | AttributeTargets.Method | AttributeTargets.Constructor | AttributeTargets.Property)] 
    public sealed class ContractVerificationAttribute : Attribute
    { 
        private bool _value; 

        public ContractVerificationAttribute(bool value) { _value = value; } 

        public bool Value {
            get { return _value; }
        } 
    }
 
    ///  
    /// Allows a field f to be used in the method contracts for a method m when f has less visibility than m.
    /// For instance, if the method is public, but the field is private. 
    /// 
    [Conditional("CONTRACTS_FULL")]
    [AttributeUsage(AttributeTargets.Field)]
    [SuppressMessage("Microsoft.Design", "CA1019:DefineAccessorsForAttributeArguments", Justification = "Thank you very much, but we like the names we've defined for the accessors")] 
    public sealed class ContractPublicPropertyNameAttribute : Attribute
    { 
        private String _publicName; 

        public ContractPublicPropertyNameAttribute(String name) 
        {
            _publicName = name;
        }
 
        public String Name {
            get { return _publicName; } 
        } 
    }
 
    #endregion Attributes

    /// 
    /// Contains static methods for representing program contracts such as preconditions, postconditions, and invariants. 
    /// 
    ///  
    /// WARNING: A binary rewriter must be used to insert runtime enforcement of these contracts. 
    /// Otherwise some contracts like Ensures can only be checked statically and will not throw exceptions during runtime when contracts are violated.
    /// Please note this class uses conditional compilation to help avoid easy mistakes.  Defining the preprocessor 
    /// symbol CONTRACTS_PRECONDITIONS will include all preconditions expressed using Contract.Requires in your
    /// build.  The symbol CONTRACTS_FULL will include postconditions and object invariants, and requires the binary rewriter.
    /// 
    public static partial class Contract 
    {
        #region User Methods 
 
        #region Assume
 
        /// 
        /// Instructs code analysis tools to assume the expression  is true even if it can not be statically proven to always be true.
        /// 
        /// Expression to assume will always be true. 
        /// 
        /// At runtime this is equivalent to an . 
        ///  
        [Pure]
        [Conditional("DEBUG")] 
        [Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        public static void Assume(bool condition)
        { 
            if (!condition) { 
                ReportFailure(ContractFailureKind.Assume, null, null, null);
            } 
        }

        /// 
        /// Instructs code analysis tools to assume the expression  is true even if it can not be statically proven to always be true. 
        /// 
        /// Expression to assume will always be true. 
        /// If it is not a constant string literal, then the contract may not be understood by tools. 
        /// 
        /// At runtime this is equivalent to an . 
        /// 
        [Pure]
        [Conditional("DEBUG")]
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif 
        public static void Assume(bool condition, String userMessage)
        { 
            if (!condition) {
                ReportFailure(ContractFailureKind.Assume, userMessage, null, null);
            }
        } 

        #endregion Assume 
 
        #region Assert
 
        /// 
        /// In debug builds, perform a runtime check that  is true.
        /// 
        /// Expression to check to always be true. 
        [Pure]
        [Conditional("DEBUG")] 
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Assert(bool condition)
        {
            if (!condition) 
                ReportFailure(ContractFailureKind.Assert, null, null, null);
        } 
 
        /// 
        /// In debug builds, perform a runtime check that  is true. 
        /// 
        /// Expression to check to always be true.
        /// If it is not a constant string literal, then the contract may not be understood by tools.
        [Pure] 
        [Conditional("DEBUG")]
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        public static void Assert(bool condition, String userMessage)
        {
            if (!condition)
                ReportFailure(ContractFailureKind.Assert, userMessage, null, null); 
        }
 
        #endregion Assert 

        #region Requires 

        /// 
        /// Specifies a contract such that the expression  must be true before the enclosing method or property is invoked.
        ///  
        /// Boolean expression representing the contract.
        ///  
        /// This call must happen at the beginning of a method or property before any other code. 
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// Use this form when backward compatibility does not force you to throw a particular exception. 
        /// 
        [Pure]
        [Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        public static void Requires(bool condition) 
        {
            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires"); 
        }

        /// 
        /// Specifies a contract such that the expression  must be true before the enclosing method or property is invoked. 
        /// 
        /// Boolean expression representing the contract. 
        /// If it is not a constant string literal, then the contract may not be understood by tools. 
        /// 
        /// This call must happen at the beginning of a method or property before any other code. 
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// Use this form when backward compatibility does not force you to throw a particular exception.
        /// 
        [Pure] 
        [Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Requires(bool condition, String userMessage) 
        {
            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
        }
 
        /// 
        /// Specifies a contract such that the expression  must be true before the enclosing method or property is invoked. 
        ///  
        /// Boolean expression representing the contract.
        ///  
        /// This call must happen at the beginning of a method or property before any other code.
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// Use this form when you want to throw a particular exception.
        ///  
        [SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")]
        [SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")] 
        [Pure] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Requires(bool condition) where TException : Exception
        {
            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires"); 
        }
 
        ///  
        /// Specifies a contract such that the expression  must be true before the enclosing method or property is invoked.
        ///  
        /// Boolean expression representing the contract.
        /// If it is not a constant string literal, then the contract may not be understood by tools.
        /// 
        /// This call must happen at the beginning of a method or property before any other code. 
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// Use this form when you want to throw a particular exception. 
        ///  
        [SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "userMessage")]
        [SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "condition")] 
        [SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter")]
        [Pure]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Requires(bool condition, String userMessage) where TException : Exception 
        { 
            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
        } 

        #endregion Requires

        #region Ensures 

        ///  
        /// Specifies a public contract such that the expression  will be true when the enclosing method or property returns normally. 
        /// 
        /// Boolean expression representing the contract.  May include  and . 
        /// 
        /// This call must happen at the beginning of a method or property before any other code.
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// The contract rewriter must be used for runtime enforcement of this postcondition. 
        /// 
        [Pure] 
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Ensures(bool condition)
        {
            AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures"); 
        }
 
        ///  
        /// Specifies a public contract such that the expression  will be true when the enclosing method or property returns normally.
        ///  
        /// Boolean expression representing the contract.  May include  and .
        /// If it is not a constant string literal, then the contract may not be understood by tools.
        /// 
        /// This call must happen at the beginning of a method or property before any other code. 
        /// This contract is exposed to clients so must only reference members at least as visible as the enclosing method.
        /// The contract rewriter must be used for runtime enforcement of this postcondition. 
        ///  
        [Pure]
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
        public static void Ensures(bool condition, String userMessage) 
        {
            AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures"); 
        } 

        ///  
        /// Specifies a contract such that if an exception of type  is thrown then the expression  will be true when the enclosing method or property terminates abnormally.
        /// 
        /// Type of exception related to this postcondition.
        /// Boolean expression representing the contract.  May include  and . 
        /// 
        /// This call must happen at the beginning of a method or property before any other code. 
        /// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method. 
        /// The contract rewriter must be used for runtime enforcement of this postcondition.
        ///  
        [Pure]
        [Conditional("CONTRACTS_FULL")]
        [SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        public static void EnsuresOnThrow(bool condition) where TException : Exception 
        {
            AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow"); 
        }

        /// 
        /// Specifies a contract such that if an exception of type  is thrown then the expression  will be true when the enclosing method or property terminates abnormally. 
        /// 
        /// Type of exception related to this postcondition. 
        /// Boolean expression representing the contract.  May include  and . 
        /// If it is not a constant string literal, then the contract may not be understood by tools.
        ///  
        /// This call must happen at the beginning of a method or property before any other code.
        /// This contract is exposed to clients so must only reference types and members at least as visible as the enclosing method.
        /// The contract rewriter must be used for runtime enforcement of this postcondition.
        ///  
        [Pure]
        [Conditional("CONTRACTS_FULL")] 
        [SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Exception type used in tools.")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void EnsuresOnThrow(bool condition, String userMessage) where TException : Exception
        {
            AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow"); 
        }
 
        #region Old, Result, and Out Parameters 

        ///  
        /// Represents the result (a.k.a. return value) of a method or property.
        /// 
        /// Type of return value of the enclosing method or property.
        /// Return value of the enclosing method or property. 
        /// 
        /// This method can only be used within the argument to the  contract. 
        ///  
        [SuppressMessage("Microsoft.Design", "CA1004:GenericMethodsShouldProvideTypeParameter", Justification = "Not intended to be called at runtime.")]
        [Pure] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif
        public static T Result() { return default(T); } 

        ///  
        /// Represents the final (output) value of an out parameter when returning from a method. 
        /// 
        /// Type of the out parameter. 
        /// The out parameter.
        /// The output value of the out parameter.
        /// 
        /// This method can only be used within the argument to the  contract. 
        /// 
        [SuppressMessage("Microsoft.Design", "CA1021:AvoidOutParameters", MessageId = "0#", Justification = "Not intended to be called at runtime.")] 
        [Pure] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)] 
#endif
        public static T ValueAtReturn(out T value) { value = default(T); return value; }

        ///  
        /// Represents the value of  as it was at the start of the method or property.
        ///  
        /// Type of .  This can be inferred. 
        /// Value to represent.  This must be a field or parameter.
        /// Value of  at the start of the method or property. 
        /// 
        /// This method can only be used within the argument to the  contract.
        /// 
        [SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "value")] 
        [Pure]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)] 
#endif
        public static T OldValue(T value) { return default(T); } 

        #endregion Old, Result, and Out Parameters

        #endregion Ensures 

        #region Invariant 
 
        /// 
        /// Specifies a contract such that the expression  will be true after every method or property on the enclosing class. 
        /// 
        /// Boolean expression representing the contract.
        /// 
        /// This contact can only be specified in a dedicated invariant method declared on a class. 
        /// This contract is not exposed to clients so may reference members less visible as the enclosing method.
        /// The contract rewriter must be used for runtime enforcement of this invariant. 
        ///  
        [Pure]
        [Conditional("CONTRACTS_FULL")] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
        public static void Invariant(bool condition) 
        {
            AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant"); 
        } 

        ///  
        /// Specifies a contract such that the expression  will be true after every method or property on the enclosing class.
        /// 
        /// Boolean expression representing the contract.
        /// If it is not a constant string literal, then the contract may not be understood by tools. 
        /// 
        /// This contact can only be specified in a dedicated invariant method declared on a class. 
        /// This contract is not exposed to clients so may reference members less visible as the enclosing method. 
        /// The contract rewriter must be used for runtime enforcement of this invariant.
        ///  
        [Pure]
        [Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static void Invariant(bool condition, String userMessage) 
        { 
            AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
        } 

        #endregion Invariant

        #region Quantifiers 

        #region ForAll 
 
        /// 
        /// Returns whether the  returns true 
        /// for all integers starting from  to  - 1.
        /// 
        /// First integer to pass to .
        /// One greater than the last integer to pass to . 
        /// Function that is evaluated from  to  - 1.
        /// true if  returns true for all integers 
        /// starting from  to  - 1. 
        /// 
        [Pure] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]  // Assumes predicate obeys CER rules.
#endif
        public static bool ForAll(int fromInclusive, int toExclusive, Predicate predicate) 
        {
            if (fromInclusive > toExclusive) 
#if INSIDE_CLR 
                throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive"));
#else 
                throw new ArgumentException("fromInclusive must be less than or equal to toExclusive.");
#endif
            if (predicate == null)
                throw new ArgumentNullException("predicate"); 
            Contract.EndContractBlock();
 
            for (int i = fromInclusive; i < toExclusive; i++) 
                if (!predicate(i)) return false;
            return true; 
        }


        ///  
        /// Returns whether the  returns true
        /// for all elements in the . 
        ///  
        /// The collection from which elements will be drawn from to pass to .
        /// Function that is evaluated on elements from . 
        /// true if and only if  returns true for all elements in
        /// .
        /// 
        [Pure] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]  // Assumes predicate & collection enumerator obey CER rules. 
#endif 
        public static bool ForAll(IEnumerable collection, Predicate predicate)
        { 
            if (collection == null)
                throw new ArgumentNullException("collection");
            if (predicate == null)
                throw new ArgumentNullException("predicate"); 
            Contract.EndContractBlock();
 
            foreach (T t in collection) 
                if (!predicate(t)) return false;
            return true; 
        }

        #endregion ForAll
 
        #region Exists
 
        ///  
        /// Returns whether the  returns true
        /// for any integer starting from  to  - 1. 
        /// 
        /// First integer to pass to .
        /// One greater than the last integer to pass to .
        /// Function that is evaluated from  to  - 1. 
        /// true if  returns true for any integer
        /// starting from  to  - 1. 
        ///  
        [Pure]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]  // Assumes predicate obeys CER rules.
#endif
        public static bool Exists(int fromInclusive, int toExclusive, Predicate predicate)
        { 
            if (fromInclusive > toExclusive)
#if INSIDE_CLR 
                throw new ArgumentException(Environment.GetResourceString("Argument_ToExclusiveLessThanFromExclusive")); 
#else
                throw new ArgumentException("fromInclusive must be less than or equal to toExclusive."); 
#endif
            if (predicate == null)
                throw new ArgumentNullException("predicate");
            Contract.EndContractBlock(); 

            for (int i = fromInclusive; i < toExclusive; i++) 
                if (predicate(i)) return true; 
            return false;
        } 

        /// 
        /// Returns whether the  returns true
        /// for any element in the . 
        /// 
        /// The collection from which elements will be drawn from to pass to . 
        /// Function that is evaluated on elements from . 
        /// true if and only if  returns true for an element in
        /// . 
        /// 
        [Pure]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]  // Assumes predicate & collection enumerator obey CER rules. 
#endif
        public static bool Exists(IEnumerable collection, Predicate predicate) 
        { 
            if (collection == null)
                throw new ArgumentNullException("collection"); 
            if (predicate == null)
                throw new ArgumentNullException("predicate");
            Contract.EndContractBlock();
 
            foreach (T t in collection)
                if (predicate(t)) return true; 
            return false; 
        }
 
        #endregion Exists

        #endregion Quantifiers
 
        #region Pointers
        // @ 
#if FEATURE_UNSAFE_CONTRACTS 
        /// 
        /// Runtime checking for pointer bounds is not currently feasible. Thus, at runtime, we just return 
        /// a very long extent for each pointer that is writable. As long as assertions are of the form
        /// WritableBytes(ptr) >= ..., the runtime assertions will not fail.
        /// The runtime value is 2^64 - 1 or 2^32 - 1.
        ///  
        [SuppressMessage("Microsoft.Performance", "CA1802", Justification = "FxCop is confused")]
        static readonly ulong MaxWritableExtent = (UIntPtr.Size == 4) ? UInt32.MaxValue : UInt64.MaxValue; 
 
        /// 
        /// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent. 
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this
        /// at the moment.
        /// 
        /// Start of memory region 
        /// The result is the number of bytes writable starting at 
        [CLSCompliant(false)] 
        [Pure] 
        [ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
        public static ulong WritableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); }
 
        /// 
        /// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent. 
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this 
        /// at the moment.
        ///  
        /// Start of memory region
        /// The result is the number of bytes writable starting at 
        [CLSCompliant(false)]
        [Pure] 
        [ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static ulong WritableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; } 

        /// 
        /// Allows specifying a writable extent for a UIntPtr, similar to SAL's writable extent.
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this 
        /// at the moment.
        ///  
        /// Start of memory region 
        /// The result is the number of bytes writable starting at 
        [CLSCompliant(false)] 
        [Pure]
        [ContractRuntimeIgnored]
        [SecurityCritical]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        //@ 

        unsafe public static ulong WritableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; } 

        /// 
        /// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent.
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this 
        /// at the moment.
        ///  
        /// Start of memory region 
        /// The result is the number of bytes readable starting at 
        [CLSCompliant(false)] 
        [Pure]
        [ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static ulong ReadableBytes(UIntPtr startAddress) { return MaxWritableExtent - startAddress.ToUInt64(); } 
 
        /// 
        /// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent. 
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this
        /// at the moment.
        /// 
        /// Start of memory region 
        /// The result is the number of bytes readable starting at 
        [CLSCompliant(false)] 
        [Pure] 
        [ContractRuntimeIgnored]
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif
        public static ulong ReadableBytes(IntPtr startAddress) { return MaxWritableExtent - (ulong)startAddress; }
 
        /// 
        /// Allows specifying a readable extent for a UIntPtr, similar to SAL's readable extent. 
        /// NOTE: this is for static checking only. No useful runtime code can be generated for this 
        /// at the moment.
        ///  
        /// Start of memory region
        /// The result is the number of bytes readable starting at 
        [CLSCompliant(false)]
        [Pure] 
        [ContractRuntimeIgnored]
        [SecurityCritical] 
#if FEATURE_RELIABILITY_CONTRACTS 
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
#endif 
        unsafe public static ulong ReadableBytes(void* startAddress) { return MaxWritableExtent - (ulong)startAddress; }
#endif // FEATURE_UNSAFE_CONTRACTS
        #endregion
 
        #region Misc.
 
        ///  
        /// Marker to indicate the end of the contract section of a method.
        ///  
        [Conditional("CONTRACTS_FULL")]
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
#endif 
        public static void EndContractBlock() { }
 
        #endregion 

        #endregion User Methods 

        #region Failure Behavior

        ///  
        /// Without contract rewriting, failing Assert/Assumes end up calling this method.
        /// Code going through the contract rewriter never calls this method. Instead, the rewriter produced failures call 
        /// Internal.ContractHelper.RaiseContractFailedEvent, followed by Internal.ContractHelper.TriggerFailure. 
        /// 
        static partial void ReportFailure(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException); 

        /// 
        /// This method is used internally to trigger a failure indicating to the "programmer" that he is using the interface incorrectly.
        /// It is NEVER used to indicate failure of actual contracts at runtime. 
        /// 
        static partial void AssertMustUseRewriter(ContractFailureKind kind, String contractKind); 
 
        #endregion
    } 

    public enum ContractFailureKind {
        Precondition,
        [SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")] 
        Postcondition,
        [SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Postcondition")] 
        PostconditionOnException, 
        Invariant,
        Assert, 
        Assume,
    }

 
}
 
 
namespace System.Diagnostics.Contracts.Internal
{ 
    public static partial class ContractHelper
    {
        #region Rewriter Failure Hooks
 
        /// 
        /// Rewriter will call this method on a contract failure to allow listeners to be notified. 
        /// The method should not perform any failure (assert/throw) itself. 
        /// 
        /// null if the event was handled and should not trigger a failure. 
        ///          Otherwise, returns the localized failure message
        [SuppressMessage("Microsoft.Design", "CA1030:UseEventsWhereAppropriate")]
#if FEATURE_UNTRUSTED_CALLERS
        [SuppressMessage("Microsoft.Portability", "CA1903:UseOnlyApiFromTargetedFramework", MessageId = "System.Security.SecuritySafeCriticalAttribute")] 
        [SecuritySafeCritical]
#endif 
        [System.Diagnostics.DebuggerNonUserCode] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)] 
#endif
        public static string RaiseContractFailedEvent(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException)
        {
            var resultFailureMessage = "Contract failed"; // default in case implementation does not assign anything. 
            RaiseContractFailedEventImplementation(failureKind, userMessage, conditionText, innerException, ref resultFailureMessage);
            return resultFailureMessage; 
        } 

 
        /// 
        /// Rewriter calls this method to get the default failure behavior.
        /// 
#if FEATURE_UNTRUSTED_CALLERS 
        [SecuritySafeCritical]
#endif 
        [System.Diagnostics.DebuggerNonUserCode] 
#if FEATURE_RELIABILITY_CONTRACTS
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)] 
#endif
        public static void TriggerFailure(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException)
        {
            TriggerFailureImplementation(kind, displayMessage, userMessage, conditionText, innerException); 
        }
 
        #endregion Rewriter Failure Hooks 

        #region Implementation Stubs 

        /// 
        /// Rewriter will call this method on a contract failure to allow listeners to be notified.
        /// The method should not perform any failure (assert/throw) itself. 
        /// This method has 3 functions:
        /// 1. Call any contract hooks (such as listeners to Contract failed events) 
        /// 2. Determine if the listeneres deem the failure as handled (then resultFailureMessage should be set to null) 
        /// 3. Produce a localized resultFailureMessage used in advertising the failure subsequently.
        ///  
        /// Should really be out (or the return value), but partial methods are not flexible enough.
        /// On exit: null if the event was handled and should not trigger a failure.
        ///          Otherwise, returns the localized failure message
        static partial void RaiseContractFailedEventImplementation(ContractFailureKind failureKind, String userMessage, String conditionText, Exception innerException, ref string resultFailureMessage); 

        ///  
        /// Implements the default failure behavior of the platform. Under the BCL, it triggers an Assert box. 
        /// 
        static partial void TriggerFailureImplementation(ContractFailureKind kind, String displayMessage, String userMessage, String conditionText, Exception innerException); 

        #endregion Implementation Stubs
    }
}  // namespace System.Diagnostics.Contracts.Internal 


// File provided for Reference Use Only by Microsoft Corporation (c) 2007.
                        

Link Menu

Network programming in C#, Network Programming in VB.NET, Network Programming in .NET
This book is available now!
Buy at Amazon US or
Buy at Amazon UK