diff --git a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj index 9055a5be..eeb4cf46 100644 --- a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj +++ b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj @@ -353,6 +353,7 @@ + @@ -893,6 +894,7 @@ Include="System.Security.Principal.WindowsPrincipal.cs" /> --> + diff --git a/Microsoft.Research/Contracts/MsCorlib/System.AggregateException.cs b/Microsoft.Research/Contracts/MsCorlib/System.AggregateException.cs new file mode 100644 index 00000000..2de9a138 --- /dev/null +++ b/Microsoft.Research/Contracts/MsCorlib/System.AggregateException.cs @@ -0,0 +1,224 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +#if NETFRAMEWORK_4_0 + +namespace System +{ + using System.Collections.Generic; + using System.Collections.ObjectModel; + using System.Diagnostics; + using System.Diagnostics.Contracts; + using System.Runtime.Serialization; + using System.Security; + // + // Summary: + // Represents one or more errors that occur during application execution. + public class AggregateException : Exception + { + // + // Summary: + // Initializes a new instance of the System.AggregateException class with a system-supplied + // message that describes the error. + //public AggregateException(); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with a specified + // message that describes the error. + // + // Parameters: + // message: + // The message that describes the exception. The caller of this constructor is required + // to ensure that this string has been localized for the current system culture. + //public AggregateException(string message); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with references + // to the inner exceptions that are the cause of this exception. + // + // Parameters: + // innerExceptions: + // The exceptions that are the cause of the current exception. + // + // Exceptions: + // T:System.ArgumentNullException: + // The innerExceptions argument is null. + // + // T:System.ArgumentException: + // An element of innerExceptions is null. + //public AggregateException(IEnumerable innerExceptions); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with references + // to the inner exceptions that are the cause of this exception. + // + // Parameters: + // innerExceptions: + // The exceptions that are the cause of the current exception. + // + // Exceptions: + // T:System.ArgumentNullException: + // The innerExceptions argument is null. + // + // T:System.ArgumentException: + // An element of innerExceptions is null. + //public AggregateException(params Exception[] innerExceptions); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with a specified + // error message and a reference to the inner exception that is the cause of this + // exception. + // + // Parameters: + // message: + // The message that describes the exception. The caller of this constructor is required + // to ensure that this string has been localized for the current system culture. + // + // innerException: + // The exception that is the cause of the current exception. If the innerException + // parameter is not null, the current exception is raised in a catch block that + // handles the inner exception. + // + // Exceptions: + // T:System.ArgumentNullException: + // The innerException argument is null. + //public AggregateException(string message, Exception innerException); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with a specified + // error message and references to the inner exceptions that are the cause of this + // exception. + // + // Parameters: + // message: + // The error message that explains the reason for the exception. + // + // innerExceptions: + // The exceptions that are the cause of the current exception. + // + // Exceptions: + // T:System.ArgumentNullException: + // The innerExceptions argument is null. + // + // T:System.ArgumentException: + // An element of innerExceptions is null. + //public AggregateException(string message, IEnumerable innerExceptions); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with a specified + // error message and references to the inner exceptions that are the cause of this + // exception. + // + // Parameters: + // message: + // The error message that explains the reason for the exception. + // + // innerExceptions: + // The exceptions that are the cause of the current exception. + // + // Exceptions: + // T:System.ArgumentNullException: + // The innerExceptions argument is null. + // + // T:System.ArgumentException: + // An element of innerExceptions is null. + //public AggregateException(string message, params Exception[] innerExceptions); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with serialized + // data. + // + // Parameters: + // info: + // The object that holds the serialized object data. + // + // context: + // The contextual information about the source or destination. + // + // Exceptions: + // T:System.ArgumentNullException: + // The info argument is null. + // + // T:System.Runtime.Serialization.SerializationException: + // The exception could not be deserialized correctly. + //[SecurityCritical] + //protected AggregateException(SerializationInfo info, StreamingContext context); + // + // Summary: + // Gets a read-only collection of the System.Exception instances that caused the + // current exception. + // + // Returns: + // Returns a read-only collection of the System.Exception instances that caused + // the current exception. + //public ReadOnlyCollection InnerExceptions { get; } + // + // Summary: + // Flattens an System.AggregateException instances into a single, new instance. + // + // Returns: + // A new, flattened System.AggregateException. + //public AggregateException Flatten(); + // + // Summary: + // Returns the System.AggregateException that is the root cause of this exception. + // + // Returns: + // Returns the System.AggregateException that is the root cause of this exception. + //public override Exception GetBaseException(); + // + // Summary: + // Initializes a new instance of the System.AggregateException class with serialized + // data. + // + // Parameters: + // info: + // The object that holds the serialized object data. + // + // context: + // The contextual information about the source or destination. + // + // Exceptions: + // T:System.ArgumentNullException: + // The info argument is null. + //[SecurityCritical] + //public override void GetObjectData(SerializationInfo info, StreamingContext context); + // + // Summary: + // Invokes a handler on each System.Exception contained by this System.AggregateException. + // + // Parameters: + // predicate: + // The predicate to execute for each exception. The predicate accepts as an argument + // the System.Exception to be processed and returns a Boolean to indicate whether + // the exception was handled. + // + // Exceptions: + // T:System.ArgumentNullException: + // The predicate argument is null. + // + // T:System.AggregateException: + // An exception contained by this System.AggregateException was not handled. + //public void Handle(Func predicate); + // + // Summary: + // Creates and returns a string representation of the current System.AggregateException. + // + // Returns: + // A string representation of the current exception. + //public override string ToString(); + } +} + +#endif diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.Task.cs b/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.Task.cs index e5772e51..a5178ddc 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.Task.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.Task.cs @@ -258,7 +258,13 @@ public Task(Action action, object state, CancellationToken cancellationT // Returns: // The System.AggregateException that caused the System.Threading.Tasks.Task // to end prematurely. - //public AggregateException Exception { get; } + public AggregateException Exception + { + get + { + return default(AggregateException); + } + } // // Summary: // Provides access to factory methods for creating System.Threading.Tasks.Task @@ -268,12 +274,12 @@ public Task(Action action, object state, CancellationToken cancellationT // The default System.Threading.Tasks.TaskFactory for the current task. public static TaskFactory Factory { - get -{ -Contract.Ensures(Contract.Result() != null); -return null; -} -} + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } // // Summary: // Gets a unique ID for this System.Threading.Tasks.Task instance. @@ -288,14 +294,26 @@ public static TaskFactory Factory // // Returns: // true if the task has completed due to being canceled; otherwise false. - //public bool IsCanceled { get; } + public bool IsCanceled + { + get + { + return default(bool); + } + } // // Summary: // Gets whether this System.Threading.Tasks.Task has completed. // // Returns: // true if the task has completed; otherwise false. - //public bool IsCompleted { get; } + public bool IsCompleted + { + get + { + return default(bool); + } + } // // Summary: // Gets whether the System.Threading.Tasks.Task completed due to an unhandled @@ -303,15 +321,26 @@ public static TaskFactory Factory // // Returns: // true if the task has thrown an unhandled exception; otherwise false. - //public bool IsFaulted { get; } + public bool IsFaulted + { + get + { + return default(bool); + } + } // // Summary: // Gets the System.Threading.Tasks.TaskStatus of this Task. // // Returns: // The current System.Threading.Tasks.TaskStatus of this task instance. - //public TaskStatus Status { get; } - + public TaskStatus Status + { + get + { + return default(TaskStatus); + } + } // Summary: // Creates a continuation that executes when the target System.Threading.Tasks.Task // completes. @@ -1545,7 +1574,162 @@ public static Task Run(Func function, CancellationTok return null; } - + // + // Summary: + // Creates a System.Threading.Tasks.Task`1 that's completed successfully with the + // specified result. + // + // Parameters: + // result: + // The result to store into the completed task. + // + // Type parameters: + // TResult: + // The type of the result returned by the task. + // + // Returns: + // The successfully completed task. + [Pure] + public static Task FromResult(TResult result) + { + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>().Exception == null); + Contract.Ensures(!Contract.Result>().IsCanceled); + Contract.Ensures(Contract.Result>().IsCompleted); + Contract.Ensures(!Contract.Result>().IsFaulted); + Contract.Ensures(Contract.Result>().Status == TaskStatus.RanToCompletion); + + return default(Task); + } +#endif + +#if NETFRAMEWORK_4_6 + // + // Summary: + // Creates a System.Threading.Tasks.Task that's completed due to cancellation with + // a specified cancellation token. + // + // Parameters: + // cancellationToken: + // The cancellation token with which to complete the task. + // + // Returns: + // The canceled task. + [Pure] + public static Task FromCanceled(CancellationToken cancellationToken) + { + Contract.Requires(cancellationToken.IsCancellationRequested); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().Exception == null); + Contract.Ensures(Contract.Result().IsCanceled); + Contract.Ensures(Contract.Result().IsCompleted); + Contract.Ensures(!Contract.Result().IsFaulted); + Contract.Ensures(Contract.Result().Status == TaskStatus.Canceled); + Contract.EnsuresOnThrow(true, "Cancellation has not been requested for cancellationToken; its IsCancellationRequested property is false."); + + return default(Task); + } + // + // Summary: + // Creates a System.Threading.Tasks.Task`1 that's completed due to cancellation + // with a specified cancellation token. + // + // Parameters: + // cancellationToken: + // The cancellation token with which to complete the task. + // + // Type parameters: + // TResult: + // The type of the result returned by the task. + // + // Returns: + // The canceled task. + [Pure] + public static Task FromCanceled(CancellationToken cancellationToken) + { + Contract.Requires(cancellationToken.IsCancellationRequested); + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>().Exception == null); + Contract.Ensures(Contract.Result>().IsCanceled); + Contract.Ensures(Contract.Result>().IsCompleted); + Contract.Ensures(!Contract.Result>().IsFaulted); + Contract.Ensures(Contract.Result>().Status == TaskStatus.Canceled); + Contract.EnsuresOnThrow(true, "Cancellation has not been requested for cancellationToken; its IsCancellationRequested property is false."); + + return default(Task); + } + // + // Summary: + // Creates a System.Threading.Tasks.Task that has completed with a specified exception. + // + // Parameters: + // exception: + // The exception with which to complete the task. + // + // Returns: + // The faulted task. + [Pure] + public static Task FromException(Exception exception) + { + Contract.Requires(exception != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().Exception == exception); + Contract.Ensures(!Contract.Result().IsCanceled); + Contract.Ensures(Contract.Result().IsCompleted); + Contract.Ensures(Contract.Result().IsFaulted); + Contract.Ensures(Contract.Result().Status == TaskStatus.Faulted); + + return default(Task); + } + // + // Summary: + // Creates a System.Threading.Tasks.Task`1 that's completed with a specified exception. + // + // Parameters: + // exception: + // The exception with which to complete the task. + // + // Type parameters: + // TResult: + // The type of the result returned by the task. + // + // Returns: + // The faulted task. + [Pure] + public static Task FromException(Exception exception) + { + Contract.Requires(exception != null); + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>().Exception == exception); + Contract.Ensures(!Contract.Result>().IsCanceled); + Contract.Ensures(Contract.Result>().IsCompleted); + Contract.Ensures(Contract.Result>().IsFaulted); + Contract.Ensures(Contract.Result>().Status == TaskStatus.Faulted); + + + return default(Task); + } + // + // Summary: + // Gets a task that has already completed successfully. + // + // Returns: + // The successfully completed task. + public static Task CompletedTask + { + [Pure] + get + { + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().Exception == null); + Contract.Ensures(!Contract.Result().IsCanceled); + Contract.Ensures(Contract.Result().IsCompleted); + Contract.Ensures(!Contract.Result().IsFaulted); + Contract.Ensures(Contract.Result().Status == TaskStatus.RanToCompletion); + + return default(Task); + } + } #endif } @@ -1790,7 +1974,7 @@ public Task(Func function, object state, CancellationToken canc // The result value of this System.Threading.Tasks.Task, which is the // same type as the task's type parameter. //[DebuggerBrowsable(DebuggerBrowsableState.Never)] - //public TResult Result { get; internal set; } + public TResult Result { get; internal set; } // Summary: // Creates a continuation that executes when the target System.Threading.Tasks.Task diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.TaskStatus.cs b/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.TaskStatus.cs new file mode 100644 index 00000000..dfe04379 --- /dev/null +++ b/Microsoft.Research/Contracts/MsCorlib/System.Threading.Tasks.TaskStatus.cs @@ -0,0 +1,64 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + + +#if NETFRAMEWORK_4_0 + +namespace System.Threading.Tasks +{ + // + // Summary: + // Represents the current stage in the lifecycle of a System.Threading.Tasks.Task. + public enum TaskStatus + { + // + // Summary: + // The task has been initialized but has not yet been scheduled. + Created = 0, + // + // Summary: + // The task is waiting to be activated and scheduled internally by the .NET Framework + // infrastructure. + WaitingForActivation = 1, + // + // Summary: + // The task has been scheduled for execution but has not yet begun executing. + WaitingToRun = 2, + // + // Summary: + // The task is running but has not yet completed. + Running = 3, + // + // Summary: + // The task has finished executing and is implicitly waiting for attached child + // tasks to complete. + WaitingForChildrenToComplete = 4, + // + // Summary: + // The task completed execution successfully. + RanToCompletion = 5, + // + // Summary: + // The task acknowledged cancellation by throwing an OperationCanceledException + // with its own CancellationToken while the token was in signaled state, or the + // task's CancellationToken was already signaled before the task started executing. + // For more information, see Task Cancellation. + Canceled = 6, + // + // Summary: + // The task completed due to an unhandled exception. + Faulted = 7 + } +} +#endif \ No newline at end of file