Move Contracts.cs (CoreCLR version) to shared CoreLib and update code to compile...
authorFilip Navara <filip.navara@gmail.com>
Thu, 27 Dec 2018 14:12:19 +0000 (15:12 +0100)
committerJan Kotas <jkotas@microsoft.com>
Thu, 27 Dec 2018 19:11:57 +0000 (09:11 -1000)
Signed-off-by: dotnet-bot <dotnet-bot@microsoft.com>
src/System.Private.CoreLib/shared/System.Private.CoreLib.Shared.projitems
src/System.Private.CoreLib/shared/System/Diagnostics/Contracts/Contracts.cs [new file with mode: 0644]

index abf6c54..1c26056 100644 (file)
     <Compile Include="$(MSBuildThisFileDirectory)System\DefaultBinder.cs" />
     <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\CodeAnalysis\SuppressMessageAttribute.cs" />
     <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\ConditionalAttribute.cs" />
+    <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\Contracts\Contracts.cs" />
     <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\Debug.cs" />
     <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\DebuggableAttribute.cs" />
     <Compile Include="$(MSBuildThisFileDirectory)System\Diagnostics\DebuggerBrowsableAttribute.cs" />
diff --git a/src/System.Private.CoreLib/shared/System/Diagnostics/Contracts/Contracts.cs b/src/System.Private.CoreLib/shared/System/Diagnostics/Contracts/Contracts.cs
new file mode 100644 (file)
index 0000000..334cea5
--- /dev/null
@@ -0,0 +1,657 @@
+// Licensed to the .NET Foundation under one or more agreements.
+// The .NET Foundation licenses this file to you under the MIT license.
+// See the LICENSE file in the project root for more information.
+
+/*============================================================
+**
+** 
+**
+** 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.
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.CodeAnalysis;
+using System.Diagnostics.Contracts;
+
+namespace System.Diagnostics.Contracts
+{
+    #region Attributes
+
+    /// <summary>
+    /// Methods and classes marked with this attribute can be used within calls to Contract methods. Such methods not make any visible state changes.
+    /// </summary>
+    [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
+    {
+    }
+
+    /// <summary>
+    /// Types marked with this attribute specify that a separate type contains the contracts for this type.
+    /// </summary>
+    [Conditional("CONTRACTS_FULL")]
+    [Conditional("DEBUG")]
+    [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; }
+        }
+    }
+
+    /// <summary>
+    /// Types marked with this attribute specify that they are a contract for the type that is the argument of the constructor.
+    /// </summary>
+    [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; }
+        }
+    }
+
+    /// <summary>
+    /// 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".
+    /// </summary>
+    [Conditional("CONTRACTS_FULL")]
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false, Inherited = false)]
+    public sealed class ContractInvariantMethodAttribute : Attribute
+    {
+    }
+
+    /// <summary>
+    /// Attribute that specifies that an assembly is a reference assembly with contracts.
+    /// </summary>
+    [AttributeUsage(AttributeTargets.Assembly)]
+    public sealed class ContractReferenceAssemblyAttribute : Attribute
+    {
+    }
+
+    /// <summary>
+    /// Methods (and properties) marked with this attribute can be used within calls to Contract methods, but have no runtime behavior associated with them.
+    /// </summary>
+    [Conditional("CONTRACTS_FULL")]
+    [AttributeUsage(AttributeTargets.Method | AttributeTargets.Property, AllowMultiple = false, Inherited = true)]
+    public sealed class ContractRuntimeIgnoredAttribute : Attribute
+    {
+    }
+
+    /// <summary>
+    /// 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.)
+    /// </summary>
+    /// <remarks>
+    /// 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.
+    /// </remarks>
+    [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; }
+        }
+    }
+
+    /// <summary>
+    /// 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.
+    /// </summary>
+    [Conditional("CONTRACTS_FULL")]
+    [AttributeUsage(AttributeTargets.Field)]
+    public sealed class ContractPublicPropertyNameAttribute : Attribute
+    {
+        private string _publicName;
+
+        public ContractPublicPropertyNameAttribute(string name)
+        {
+            _publicName = name;
+        }
+
+        public string Name
+        {
+            get { return _publicName; }
+        }
+    }
+
+    /// <summary>
+    /// Enables factoring legacy if-then-throw into separate methods for reuse and full control over
+    /// thrown exception and arguments
+    /// </summary>
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
+    [Conditional("CONTRACTS_FULL")]
+    public sealed class ContractArgumentValidatorAttribute : Attribute
+    {
+    }
+
+    /// <summary>
+    /// Enables writing abbreviations for contracts that get copied to other methods
+    /// </summary>
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
+    [Conditional("CONTRACTS_FULL")]
+    public sealed class ContractAbbreviatorAttribute : Attribute
+    {
+    }
+
+    /// <summary>
+    /// Allows setting contract and tool options at assembly, type, or method granularity.
+    /// </summary>
+    [AttributeUsage(AttributeTargets.All, AllowMultiple = true, Inherited = false)]
+    [Conditional("CONTRACTS_FULL")]
+    public sealed class ContractOptionAttribute : Attribute
+    {
+        private string _category;
+        private string _setting;
+        private bool _enabled;
+        private string _value;
+
+        public ContractOptionAttribute(string category, string setting, bool enabled)
+        {
+            _category = category;
+            _setting = setting;
+            _enabled = enabled;
+        }
+
+        public ContractOptionAttribute(string category, string setting, string value)
+        {
+            _category = category;
+            _setting = setting;
+            _value = value;
+        }
+
+        public string Category
+        {
+            get { return _category; }
+        }
+
+        public string Setting
+        {
+            get { return _setting; }
+        }
+
+        public bool Enabled
+        {
+            get { return _enabled; }
+        }
+
+        public string Value
+        {
+            get { return _value; }
+        }
+    }
+
+    #endregion Attributes
+
+    /// <summary>
+    /// Contains static methods for representing program contracts such as preconditions, postconditions, and invariants.
+    /// </summary>
+    /// <remarks>
+    /// 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.
+    /// </remarks>
+    public static partial class Contract
+    {
+        #region User Methods
+
+        #region Assume
+
+        /// <summary>
+        /// Instructs code analysis tools to assume the expression <paramref name="condition"/> is true even if it can not be statically proven to always be true.
+        /// </summary>
+        /// <param name="condition">Expression to assume will always be true.</param>
+        /// <remarks>
+        /// At runtime this is equivalent to an <seealso cref="System.Diagnostics.Contracts.Contract.Assert(bool)"/>.
+        /// </remarks>
+        [Pure]
+        [Conditional("DEBUG")]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Assume(bool condition)
+        {
+            if (!condition)
+            {
+                ReportFailure(ContractFailureKind.Assume, null, null, null);
+            }
+        }
+
+        /// <summary>
+        /// Instructs code analysis tools to assume the expression <paramref name="condition"/> is true even if it can not be statically proven to always be true.
+        /// </summary>
+        /// <param name="condition">Expression to assume will always be true.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// At runtime this is equivalent to an <seealso cref="System.Diagnostics.Contracts.Contract.Assert(bool)"/>.
+        /// </remarks>
+        [Pure]
+        [Conditional("DEBUG")]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Assume(bool condition, string userMessage)
+        {
+            if (!condition)
+            {
+                ReportFailure(ContractFailureKind.Assume, userMessage, null, null);
+            }
+        }
+
+        #endregion Assume
+
+        #region Assert
+
+        /// <summary>
+        /// In debug builds, perform a runtime check that <paramref name="condition"/> is true.
+        /// </summary>
+        /// <param name="condition">Expression to check to always be true.</param>
+        [Pure]
+        [Conditional("DEBUG")]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Assert(bool condition)
+        {
+            if (!condition)
+                ReportFailure(ContractFailureKind.Assert, null, null, null);
+        }
+
+        /// <summary>
+        /// In debug builds, perform a runtime check that <paramref name="condition"/> is true.
+        /// </summary>
+        /// <param name="condition">Expression to check to always be true.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        [Pure]
+        [Conditional("DEBUG")]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Assert(bool condition, string userMessage)
+        {
+            if (!condition)
+                ReportFailure(ContractFailureKind.Assert, userMessage, null, null);
+        }
+
+        #endregion Assert
+
+        #region Requires
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> must be true before the enclosing method or property is invoked.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Requires(bool condition)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> must be true before the enclosing method or property is invoked.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Requires(bool condition, string userMessage)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> must be true before the enclosing method or property is invoked.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        public static void Requires<TException>(bool condition) where TException : Exception
+        {
+            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires<TException>");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> must be true before the enclosing method or property is invoked.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        public static void Requires<TException>(bool condition, string userMessage) where TException : Exception
+        {
+            AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires<TException>");
+        }
+
+        #endregion Requires
+
+        #region Ensures
+
+        /// <summary>
+        /// Specifies a public contract such that the expression <paramref name="condition"/> will be true when the enclosing method or property returns normally.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.  May include <seealso cref="OldValue"/> and <seealso cref="Result"/>.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Ensures(bool condition)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
+        }
+
+        /// <summary>
+        /// Specifies a public contract such that the expression <paramref name="condition"/> will be true when the enclosing method or property returns normally.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.  May include <seealso cref="OldValue"/> and <seealso cref="Result"/>.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Ensures(bool condition, string userMessage)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Postcondition, "Ensures");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that if an exception of type <typeparamref name="TException"/> is thrown then the expression <paramref name="condition"/> will be true when the enclosing method or property terminates abnormally.
+        /// </summary>
+        /// <typeparam name="TException">Type of exception related to this postcondition.</typeparam>
+        /// <param name="condition">Boolean expression representing the contract.  May include <seealso cref="OldValue"/> and <seealso cref="Result"/>.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void EnsuresOnThrow<TException>(bool condition) where TException : Exception
+        {
+            AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that if an exception of type <typeparamref name="TException"/> is thrown then the expression <paramref name="condition"/> will be true when the enclosing method or property terminates abnormally.
+        /// </summary>
+        /// <typeparam name="TException">Type of exception related to this postcondition.</typeparam>
+        /// <param name="condition">Boolean expression representing the contract.  May include <seealso cref="OldValue"/> and <seealso cref="Result"/>.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void EnsuresOnThrow<TException>(bool condition, string userMessage) where TException : Exception
+        {
+            AssertMustUseRewriter(ContractFailureKind.PostconditionOnException, "EnsuresOnThrow");
+        }
+
+        #region Old, Result, and Out Parameters
+
+        /// <summary>
+        /// Represents the result (a.k.a. return value) of a method or property.
+        /// </summary>
+        /// <typeparam name="T">Type of return value of the enclosing method or property.</typeparam>
+        /// <returns>Return value of the enclosing method or property.</returns>
+        /// <remarks>
+        /// This method can only be used within the argument to the <seealso cref="Ensures(bool)"/> contract.
+        /// </remarks>
+        [Pure]
+        public static T Result<T>() { return default; }
+
+        /// <summary>
+        /// Represents the final (output) value of an out parameter when returning from a method.
+        /// </summary>
+        /// <typeparam name="T">Type of the out parameter.</typeparam>
+        /// <param name="value">The out parameter.</param>
+        /// <returns>The output value of the out parameter.</returns>
+        /// <remarks>
+        /// This method can only be used within the argument to the <seealso cref="Ensures(bool)"/> contract.
+        /// </remarks>
+        [Pure]
+        public static T ValueAtReturn<T>(out T value) { value = default; return value; }
+
+        /// <summary>
+        /// Represents the value of <paramref name="value"/> as it was at the start of the method or property.
+        /// </summary>
+        /// <typeparam name="T">Type of <paramref name="value"/>.  This can be inferred.</typeparam>
+        /// <param name="value">Value to represent.  This must be a field or parameter.</param>
+        /// <returns>Value of <paramref name="value"/> at the start of the method or property.</returns>
+        /// <remarks>
+        /// This method can only be used within the argument to the <seealso cref="Ensures(bool)"/> contract.
+        /// </remarks>
+        [Pure]
+        public static T OldValue<T>(T value) { return default; }
+
+        #endregion Old, Result, and Out Parameters
+
+        #endregion Ensures
+
+        #region Invariant
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> will be true after every method or property on the enclosing class.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Invariant(bool condition)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
+        }
+
+        /// <summary>
+        /// Specifies a contract such that the expression <paramref name="condition"/> will be true after every method or property on the enclosing class.
+        /// </summary>
+        /// <param name="condition">Boolean expression representing the contract.</param>
+        /// <param name="userMessage">If it is not a constant string literal, then the contract may not be understood by tools.</param>
+        /// <remarks>
+        /// 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.
+        /// </remarks>
+        [Pure]
+        [Conditional("CONTRACTS_FULL")]
+        public static void Invariant(bool condition, string userMessage)
+        {
+            AssertMustUseRewriter(ContractFailureKind.Invariant, "Invariant");
+        }
+
+        #endregion Invariant
+
+        #region Quantifiers
+
+        #region ForAll
+
+        /// <summary>
+        /// Returns whether the <paramref name="predicate"/> returns <c>true</c> 
+        /// for all integers starting from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.
+        /// </summary>
+        /// <param name="fromInclusive">First integer to pass to <paramref name="predicate"/>.</param>
+        /// <param name="toExclusive">One greater than the last integer to pass to <paramref name="predicate"/>.</param>
+        /// <param name="predicate">Function that is evaluated from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.</param>
+        /// <returns><c>true</c> if <paramref name="predicate"/> returns <c>true</c> for all integers 
+        /// starting from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.</returns>
+        /// <seealso cref="System.Collections.Generic.List&lt;T&gt;.TrueForAll"/>
+        [Pure]
+        public static bool ForAll(int fromInclusive, int toExclusive, Predicate<int> predicate)
+        {
+            if (fromInclusive > toExclusive)
+                throw new ArgumentException(SR.Argument_ToExclusiveLessThanFromExclusive);
+            if (predicate == null)
+                throw new ArgumentNullException(nameof(predicate));
+
+            for (int i = fromInclusive; i < toExclusive; i++)
+                if (!predicate(i)) return false;
+            return true;
+        }
+
+
+        /// <summary>
+        /// Returns whether the <paramref name="predicate"/> returns <c>true</c> 
+        /// for all elements in the <paramref name="collection"/>.
+        /// </summary>
+        /// <param name="collection">The collection from which elements will be drawn from to pass to <paramref name="predicate"/>.</param>
+        /// <param name="predicate">Function that is evaluated on elements from <paramref name="collection"/>.</param>
+        /// <returns><c>true</c> if and only if <paramref name="predicate"/> returns <c>true</c> for all elements in
+        /// <paramref name="collection"/>.</returns>
+        /// <seealso cref="System.Collections.Generic.List&lt;T&gt;.TrueForAll"/>
+        [Pure]
+        public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate)
+        {
+            if (collection == null)
+                throw new ArgumentNullException(nameof(collection));
+            if (predicate == null)
+                throw new ArgumentNullException(nameof(predicate));
+
+            foreach (T t in collection)
+                if (!predicate(t)) return false;
+            return true;
+        }
+
+        #endregion ForAll
+
+        #region Exists
+
+        /// <summary>
+        /// Returns whether the <paramref name="predicate"/> returns <c>true</c> 
+        /// for any integer starting from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.
+        /// </summary>
+        /// <param name="fromInclusive">First integer to pass to <paramref name="predicate"/>.</param>
+        /// <param name="toExclusive">One greater than the last integer to pass to <paramref name="predicate"/>.</param>
+        /// <param name="predicate">Function that is evaluated from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.</param>
+        /// <returns><c>true</c> if <paramref name="predicate"/> returns <c>true</c> for any integer
+        /// starting from <paramref name="fromInclusive"/> to <paramref name="toExclusive"/> - 1.</returns>
+        /// <seealso cref="System.Collections.Generic.List&lt;T&gt;.Exists"/>
+        [Pure]
+        public static bool Exists(int fromInclusive, int toExclusive, Predicate<int> predicate)
+        {
+            if (fromInclusive > toExclusive)
+                throw new ArgumentException(SR.Argument_ToExclusiveLessThanFromExclusive);
+            if (predicate == null)
+                throw new ArgumentNullException(nameof(predicate));
+
+            for (int i = fromInclusive; i < toExclusive; i++)
+                if (predicate(i)) return true;
+            return false;
+        }
+
+        /// <summary>
+        /// Returns whether the <paramref name="predicate"/> returns <c>true</c> 
+        /// for any element in the <paramref name="collection"/>.
+        /// </summary>
+        /// <param name="collection">The collection from which elements will be drawn from to pass to <paramref name="predicate"/>.</param>
+        /// <param name="predicate">Function that is evaluated on elements from <paramref name="collection"/>.</param>
+        /// <returns><c>true</c> if and only if <paramref name="predicate"/> returns <c>true</c> for an element in
+        /// <paramref name="collection"/>.</returns>
+        /// <seealso cref="System.Collections.Generic.List&lt;T&gt;.Exists"/>
+        [Pure]
+        public static bool Exists<T>(IEnumerable<T> collection, Predicate<T> predicate)
+        {
+            if (collection == null)
+                throw new ArgumentNullException(nameof(collection));
+            if (predicate == null)
+                throw new ArgumentNullException(nameof(predicate));
+
+            foreach (T t in collection)
+                if (predicate(t)) return true;
+            return false;
+        }
+
+        #endregion Exists
+
+        #endregion Quantifiers
+
+        #region Pointers
+        #endregion
+
+        #region Misc.
+
+        /// <summary>
+        /// Marker to indicate the end of the contract section of a method.
+        /// </summary>
+        [Conditional("CONTRACTS_FULL")]
+        public static void EndContractBlock() { }
+
+        #endregion
+
+        #endregion User Methods
+    }
+
+    [System.Runtime.CompilerServices.TypeForwardedFrom("mscorlib, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089")]
+    public enum ContractFailureKind
+    {
+        Precondition,
+        Postcondition,
+        PostconditionOnException,
+        Invariant,
+        Assert,
+        Assume,
+    }
+}  // namespace System.Runtime.CompilerServices
+