--- /dev/null
+// 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<T>.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<T>.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<T>.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<T>.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
+