Add contracts to System.Windows.Forms, System.Windows.Data classes

Microsoft.Research/Contracts/System.Data/System.Data.Common.DbParameterCollection.cs

@@ -12,17 +12,13 @@
 // 
 // 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.
 
-using System;
-using System.Collections;
-using System.ComponentModel;
-using System.Data;
-using System.Reflection;
 using System.Diagnostics.Contracts;
 
 namespace System.Data.Common
 {
   // Summary:
   //     The base class for a collection of parameters relevant to a System.Data.Common.DbCommand.
+  [ContractClass(typeof(DbParameterCollectionContract))]
   public abstract class DbParameterCollection //: MarshalByRefObject, IDataParameterCollection, IList, ICollection, IEnumerable
   {
     // Summary:
@@ -37,7 +33,7 @@ public abstract class DbParameterCollection //: MarshalByRefObject, IDataParamet
     //     The number of items in the collection.
     //rowsable(false)]
     //[DesignerSerializationVisibility(DesignerSerializationVisibility.Hidden)]
-    //public abstract int Count { get; }
+    public abstract int Count { get; }
     //
     // Summary:
     //     Specifies whether the collection is a fixed size.
@@ -121,7 +117,17 @@ public DbParameter this[int index]
     // Exceptions:
     //   System.IndexOutOfRangeException:
     //     The specified index does not exist.
-    //public DbParameter this[string parameterName] { get; set; }
+    public DbParameter this[string parameterName]
+		{
+			get
+			{
+				return default(DbParameter);
+			}
+			set
+			{
+
+			}
+		}
 
     // Summary:
     //     Adds a System.Data.Common.DbParameter item with the specified value to the
@@ -134,15 +140,15 @@ public DbParameter this[int index]
     //
     // Returns:
     //     The index of the System.Data.Common.DbParameter object in the collection.
-    //public abstract int Add(object value);
+    public abstract int Add(object value);
     //
     // Summary:
     //     Adds an array of items with the specified values to the System.Data.Common.DbParameterCollection.
     //
     // Parameters:
     //   values:
     //     An array of values of type System.Data.Common.DbParameter to add to the collection.
-    //public abstract void AddRange(Array values);
+    public abstract void AddRange(Array values);
     //
     // Summary:
     //     Removes all System.Data.Common.DbParameter values from the System.Data.Common.DbParameterCollection.
@@ -305,4 +311,34 @@ public DbParameter this[int index]
     //     The new System.Data.Common.DbParameter value.
     //protected abstract void SetParameter(string parameterName, DbParameter value);
   }
+
+	[ContractClassFor(typeof(DbParameterCollection))]
+	abstract class DbParameterCollectionContract : DbParameterCollection
+	{
+		private DbParameterCollectionContract()
+		{
+
+		}
+
+		public override int Add(object value)
+		{
+			Contract.Requires(value != null);
+			Contract.Ensures(Contract.Result<int>() >= 0);
+			return default(int);
+		}
+
+		public override void AddRange(Array values)
+		{
+			Contract.Requires(values != null);
+		}
+
+		public override int Count
+		{
+			get
+			{
+				Contract.Ensures(Contract.Result<int>() >= 0);
+				return default(int);
+			}
+		}
+	}
 }

Microsoft.Research/Contracts/System.Data/System.Data.SqlClient.SqlCommand.cs

@@ -180,7 +180,14 @@ namespace System.Data.SqlClient
     //[ResCategory("DataCategory_Data")]
     //[DesignerSerializationVisibility(DesignerSerializationVisibility.Content)]
     //[ResDescription("DbCommand_Parameters")]
-    //public SqlParameterCollection Parameters { get; }
+    public SqlParameterCollection Parameters
+	{
+		get
+		{
+				Contract.Ensures(Contract.Result<SqlParameterCollection>() != null);
+				return default(SqlParameterCollection);
+		}
+	}
     //
     // Summary:
     //     Gets or sets the System.Data.SqlClient.SqlTransaction within which the System.Data.SqlClient.SqlCommand

Microsoft.Research/Contracts/System.Data/System.Data.SqlClient.SqlParameter.cs

@@ -31,7 +31,10 @@ namespace System.Data.SqlClient
   {
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class.
-    //public SqlParameter();
+    public SqlParameter()
+	{
+
+	}
     //
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class
@@ -43,7 +46,10 @@ namespace System.Data.SqlClient
     //
     //   value:
     //     An System.Object that is the value of the System.Data.SqlClient.SqlParameter.
-    //public SqlParameter(string parameterName, object value);
+    public SqlParameter(string parameterName, object value)
+	{
+
+	}
     //
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class
@@ -59,7 +65,10 @@ namespace System.Data.SqlClient
     // Exceptions:
     //   System.ArgumentException:
     //     The value supplied in the dbType parameter is an invalid back-end data type.
-    //public SqlParameter(string parameterName, SqlDbType dbType);
+    public SqlParameter(string parameterName, SqlDbType dbType)
+	{
+
+	}
     //
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class
@@ -78,7 +87,10 @@ namespace System.Data.SqlClient
     // Exceptions:
     //   System.ArgumentException:
     //     The value supplied in the dbType parameter is an invalid back-end data type.
-    //public SqlParameter(string parameterName, SqlDbType dbType, int size);
+    public SqlParameter(string parameterName, SqlDbType dbType, int size)
+	{
+
+	}
     //
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class
@@ -101,7 +113,10 @@ namespace System.Data.SqlClient
     // Exceptions:
     //   System.ArgumentException:
     //     The value supplied in the dbType parameter is an invalid back-end data type.
-    //public SqlParameter(string parameterName, SqlDbType dbType, int size, string sourceColumn);
+    public SqlParameter(string parameterName, SqlDbType dbType, int size, string sourceColumn)
+	{
+
+	}
     //
     // Summary:
     //     Initializes a new instance of the System.Data.SqlClient.SqlParameter class

Microsoft.Research/Contracts/System.Data/System.Data.SqlClient.SqlParameterCollection.cs

@@ -0,0 +1,112 @@
+// 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.
+
+using System.Data.Common;
+using System.Diagnostics.Contracts;
+
+namespace System.Data.SqlClient
+{
+	public sealed class SqlParameterCollection : DbParameterCollection
+	{
+		internal SqlParameterCollection()
+		{
+		}
+
+		public SqlParameter Add(SqlParameter value)
+		{
+			Contract.Ensures(value == null || Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public override int Add(object value)
+		{
+			return default(int);
+		}
+
+		public SqlParameter Add(string parameterName, SqlDbType sqlDbType)
+		{
+			Contract.Ensures(Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public SqlParameter Add(string parameterName, object value)
+		{
+			Contract.Ensures(Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public SqlParameter Add(string parameterName, SqlDbType sqlDbType, int size)
+		{
+			Contract.Ensures(Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public SqlParameter Add(string parameterName, SqlDbType sqlDbType, int size, string sourceColumn)
+		{
+			Contract.Ensures(Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public void AddRange(SqlParameter[] values)
+		{
+			Contract.Requires(values != null);
+		}
+
+		public override void AddRange(Array values)
+		{
+		}
+
+		public SqlParameter AddWithValue(string parameterName, object value)
+		{
+			Contract.Ensures(Contract.Result<SqlParameter>() != null);
+			return default(SqlParameter);
+		}
+
+		public override int Count
+		{
+			get
+			{
+				return default(int);
+			}
+		}
+
+		public new SqlParameter this[int index]
+		{
+			get
+			{
+				Contract.Ensures(Contract.Result<SqlParameter>() != null);
+				return default(SqlParameter);
+			}
+			set
+			{
+				Contract.Requires(value != null);
+				Contract.Requires(index >= 0);
+				Contract.Requires(index < this.Count);
+			}
+		}
+
+		public new SqlParameter this[string parameterName]
+		{
+			get
+			{
+				Contract.Ensures(Contract.Result<SqlParameter>() != null);
+				return default(SqlParameter);
+			}
+			set
+			{
+
+			}
+		}
+	}
+}

Microsoft.Research/Contracts/System.Data/System.Data.SqlDbType.cs

@@ -0,0 +1,51 @@
+// 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.
+
+namespace System.Data
+{
+	public enum SqlDbType
+	{
+		BigInt = 0,
+		Binary = 1,
+		Bit = 2,
+		Char = 3,
+		Date = 0x1f,
+		DateTime = 4,
+		DateTime2 = 0x21,
+		DateTimeOffset = 0x22,
+		Decimal = 5,
+		Float = 6,
+		Image = 7,
+		Int = 8,
+		Money = 9,
+		NChar = 10,
+		NText = 11,
+		NVarChar = 12,
+		Real = 13,
+		SmallDateTime = 15,
+		SmallInt = 0x10,
+		SmallMoney = 0x11,
+		Structured = 30,
+		Text = 0x12,
+		Time = 0x20,
+		Timestamp = 0x13,
+		TinyInt = 20,
+		Udt = 0x1d,
+		UniqueIdentifier = 14,
+		VarBinary = 0x15,
+		VarChar = 0x16,
+		Variant = 0x17,
+		Xml = 0x19
+	}
+}

Microsoft.Research/Contracts/System.Data/System.Data10.csproj

@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <PropertyGroup>
     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -222,6 +222,8 @@
     <Compile Include="System.Data.SqlClient.SqlCommandBuilder.cs" />
     <Compile Include="System.Data.SqlClient.SqlDataReader.cs" />
     <Compile Include="System.Data.SqlClient.SqlParameter.cs" />
+    <Compile Include="System.Data.SqlClient.SqlParameterCollection.cs" />
+    <Compile Include="System.Data.SqlDbType.cs" />
     <Compile Include="System.Data.SqlTypes.SqlBinary.cs" />
     <Compile Include="System.Data.SqlTypes.SqlBoolean.cs" />
     <Compile Include="System.Data.SqlTypes.SqlByte.cs" />
@@ -299,4 +301,4 @@
   <Target Name="AfterBuild">
   </Target>
   -->
-</Project>
+</Project>