diff --git a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj index 047c523c..8518d5d8 100644 --- a/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj +++ b/Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj @@ -328,8 +328,11 @@ + + + @@ -848,6 +851,7 @@ Include="System.Security.Principal.WindowsPrincipal.cs" /> --> + diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Collections.Generic.IDictionary.cs b/Microsoft.Research/Contracts/MsCorlib/System.Collections.Generic.IDictionary.cs index feb13afd..e02ef420 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Collections.Generic.IDictionary.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Collections.Generic.IDictionary.cs @@ -167,11 +167,13 @@ TValue IDictionary.this[TKey key] { get { + Contract.Requires(!ReferenceEquals(key, null)); // Contract.Requires(ContainsKey(key)); throw new NotImplementedException(); } set { + Contract.Requires(!ReferenceEquals(key, null)); // Contract.Ensures(ContainsKey(key)); //Contract.Ensures(old(ContainsKey(key)) ==> Count == old(Count)); //Contract.Ensures(!old(ContainsKey(key)) ==> Count == old(Count) + 1); @@ -181,29 +183,31 @@ TValue IDictionary.this[TKey key] void IDictionary.Add(TKey key, TValue value) { + Contract.Requires(!ReferenceEquals(key, null)); // Contract.Requires(!ContainsKey(key)); //modifies this.*; //Contract.Ensures(ContainsKey(key)); } - bool IDictionary.ContainsKey(TKey key) + public bool ContainsKey(TKey key) { - var @this = (IDictionary)this; - Contract.Ensures(!Contract.Result() || @this.Count > 0); + Contract.Requires(!ReferenceEquals(key, null)); + Contract.Ensures(!Contract.Result() || (Count > 0)); throw new NotImplementedException(); } bool IDictionary.Remove(TKey key) { + Contract.Requires(!ReferenceEquals(key, null)); // Contract.Ensures(!Contract.Result() || Contract.OldValue(ContainsKey(key)) && !ContainsKey(key)); throw new NotImplementedException(); } bool IDictionary.TryGetValue(TKey key, out TValue value) { - var @this = (IDictionary)this; - Contract.Ensures(Contract.Result() == @this.ContainsKey(key)); + Contract.Requires(!ReferenceEquals(key, null)); + Contract.Ensures(Contract.Result() == ContainsKey(key)); throw new NotImplementedException(); } @@ -211,7 +215,7 @@ bool IDictionary.TryGetValue(TKey key, out TValue value) #region ICollection> Members - int ICollection>.Count + public int Count { get { throw new NotImplementedException(); } } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Collections.ObjectModel.Collection.cs b/Microsoft.Research/Contracts/MsCorlib/System.Collections.ObjectModel.Collection.cs new file mode 100644 index 00000000..099c91c1 --- /dev/null +++ b/Microsoft.Research/Contracts/MsCorlib/System.Collections.ObjectModel.Collection.cs @@ -0,0 +1,395 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using System.Reflection; +using System.Runtime; +using System.Runtime.InteropServices; + +namespace System.Collections.ObjectModel +{ + // Summary: + // Provides the base class for a generic collection. + // + // Type parameters: + // T: + // The type of elements in the collection. + public class Collection : IList, ICollection, IEnumerable, IList, ICollection, IEnumerable + { + // Summary: + // Initializes a new instance of the System.Collections.ObjectModel.Collection + // class that is empty. + public Collection() + { + } + + // + // Summary: + // Initializes a new instance of the System.Collections.ObjectModel.Collection + // class as a wrapper for the specified list. + // + // Parameters: + // list: + // The list that is wrapped by the new collection. + // + // Exceptions: + // System.ArgumentNullException: + // list is null. + public Collection(IList list) + { + Contract.Requires(list != null); + } + + // Summary: + // Gets the number of elements actually contained in the System.Collections.ObjectModel.Collection. + // + // Returns: + // The number of elements actually contained in the System.Collections.ObjectModel.Collection. + public int Count + { + get + { + return 0; + } + } + + bool ICollection.IsSynchronized + { + get + { + throw new NotImplementedException(); + } + } + + object ICollection.SyncRoot + { + get + { + throw new NotImplementedException(); + } + } + + void ICollection.CopyTo(Array array, int index) + { + throw new NotImplementedException(); + } + + bool IList.IsFixedSize + { + get + { + throw new NotImplementedException(); + } + } + + bool IList.IsReadOnly + { + get + { + throw new NotImplementedException(); + } + } + + object IList.this[int index] + { + get + { + throw new NotImplementedException(); + } + set + { + throw new NotImplementedException(); + } + } + + bool ICollection.IsReadOnly + { + get + { + throw new NotImplementedException(); + } + } + + // + // Summary: + // Gets a System.Collections.Generic.IList wrapper around the System.Collections.ObjectModel.Collection. + // + // Returns: + // A System.Collections.Generic.IList wrapper around the System.Collections.ObjectModel.Collection. + protected IList Items + { + get + { + Contract.Ensures(Contract.Result>() != null); + return null; + } + } + + // Summary: + // Gets or sets the element at the specified index. + // + // Parameters: + // index: + // The zero-based index of the element to get or set. + // + // Returns: + // The element at the specified index. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is equal to or greater than System.Collections.ObjectModel.Collection.Count. + public T this[int index] { + get + { + return default(T); + } + set + { + } + } + + // Summary: + // Adds an object to the end of the System.Collections.ObjectModel.Collection. + // + // Parameters: + // item: + // The object to be added to the end of the System.Collections.ObjectModel.Collection. + // The value can be null for reference types. + public void Add(T item) + { + + } + // + // Summary: + // Removes all elements from the System.Collections.ObjectModel.Collection. + + int IList.Add(object value) + { + throw new NotImplementedException(); + } + + public void Clear() + { + + } + + bool IList.Contains(object value) + { + throw new NotImplementedException(); + } + + int IList.IndexOf(object value) + { + throw new NotImplementedException(); + } + + void IList.Insert(int index, object value) + { + throw new NotImplementedException(); + } + + void IList.Remove(object value) + { + throw new NotImplementedException(); + } + + // + // Summary: + // Removes all elements from the System.Collections.ObjectModel.Collection. + protected virtual void ClearItems() + { + + } + // + // Summary: + // Determines whether an element is in the System.Collections.ObjectModel.Collection. + // + // Parameters: + // item: + // The object to locate in the System.Collections.ObjectModel.Collection. + // The value can be null for reference types. + // + // Returns: + // true if item is found in the System.Collections.ObjectModel.Collection; + // otherwise, false. + public bool Contains(T item) + { + return false; + } + // + // Summary: + // Copies the entire System.Collections.ObjectModel.Collection to a compatible + // one-dimensional System.Array, starting at the specified index of the target + // array. + // + // Parameters: + // array: + // The one-dimensional System.Array that is the destination of the elements + // copied from System.Collections.ObjectModel.Collection. The System.Array + // must have zero-based indexing. + // + // index: + // The zero-based index in array at which copying begins. + // + // Exceptions: + // System.ArgumentNullException: + // array is null. + // + // System.ArgumentOutOfRangeException: + // index is less than zero. + // + // System.ArgumentException: + // The number of elements in the source System.Collections.ObjectModel.Collection + // is greater than the available space from index to the end of the destination + // array. + public void CopyTo(T[] array, int index) + { + + } + // + // Summary: + // Returns an enumerator that iterates through the System.Collections.ObjectModel.Collection. + // + // Returns: + // An System.Collections.Generic.IEnumerator for the System.Collections.ObjectModel.Collection. + public IEnumerator GetEnumerator() + { + return null; + } + + [ContractModel] + public object[] Model + { + [ContractRuntimeIgnored] + get + { + throw new NotImplementedException(); + } + } + + // + // Summary: + // Searches for the specified object and returns the zero-based index of the + // first occurrence within the entire System.Collections.ObjectModel.Collection. + // + // Parameters: + // item: + // The object to locate in the System.Collections.Generic.List. The value + // can be null for reference types. + // + // Returns: + // The zero-based index of the first occurrence of item within the entire System.Collections.ObjectModel.Collection, + // if found; otherwise, -1. + public int IndexOf(T item) + { + return 0; + } + // + // Summary: + // Inserts an element into the System.Collections.ObjectModel.Collection + // at the specified index. + // + // Parameters: + // index: + // The zero-based index at which item should be inserted. + // + // item: + // The object to insert. The value can be null for reference types. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is greater than System.Collections.ObjectModel.Collection.Count. + public void Insert(int index, T item) + { + + } + // + // Summary: + // Inserts an element into the System.Collections.ObjectModel.Collection + // at the specified index. + // + // Parameters: + // index: + // The zero-based index at which item should be inserted. + // + // item: + // The object to insert. The value can be null for reference types. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is greater than System.Collections.ObjectModel.Collection.Count. + protected virtual void InsertItem(int index, T item) + { + Contract.Requires((index >= 0) && (index <= Count)); + } + // + // Summary: + // Removes the first occurrence of a specific object from the System.Collections.ObjectModel.Collection. + // + // Parameters: + // item: + // The object to remove from the System.Collections.ObjectModel.Collection. + // The value can be null for reference types. + // + // Returns: + // true if item is successfully removed; otherwise, false. This method also + // returns false if item was not found in the original System.Collections.ObjectModel.Collection. + public bool Remove(T item) + { + return false; + } + // + // Summary: + // Removes the element at the specified index of the System.Collections.ObjectModel.Collection. + // + // Parameters: + // index: + // The zero-based index of the element to remove. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is equal to or greater than System.Collections.ObjectModel.Collection.Count. + public void RemoveAt(int index) { } + // + // Summary: + // Removes the element at the specified index of the System.Collections.ObjectModel.Collection. + // + // Parameters: + // index: + // The zero-based index of the element to remove. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is equal to or greater than System.Collections.ObjectModel.Collection.Count. + protected virtual void RemoveItem(int index) + { + Contract.Requires((index >= 0) && (index < Count)); + } + // + // Summary: + // Replaces the element at the specified index. + // + // Parameters: + // index: + // The zero-based index of the element to replace. + // + // item: + // The new value for the element at the specified index. The value can be null + // for reference types. + // + // Exceptions: + // System.ArgumentOutOfRangeException: + // index is less than zero.-or-index is greater than System.Collections.ObjectModel.Collection.Count. + protected virtual void SetItem(int index, T item) + { + // Comment is wrong, index must be < Count! + Contract.Requires((index >= 0) && (index < Count)); + } + + IEnumerator IEnumerable.GetEnumerator() + { + return GetEnumerator(); + } + } +} diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CalendarWeekRule.cs b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CalendarWeekRule.cs index 57cf7277..3d1f53db 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CalendarWeekRule.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CalendarWeekRule.cs @@ -22,8 +22,6 @@ namespace System.Globalization { // Summary: // Defines different rules for determining the first week of the year. - [Serializable] - [ComVisible(true)] public enum CalendarWeekRule { // Summary: // Indicates that the first week of the year starts on the first day of the diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs index feb8a39d..8b90ebc9 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.CultureInfo.cs @@ -18,6 +18,19 @@ namespace System.Globalization { +#if !SILVERLIGHT + public enum CultureTypes + { + NeutralCultures = 1, + SpecificCultures = 2, + InstalledWin32Cultures = 4, + AllCultures = InstalledWin32Cultures | SpecificCultures | NeutralCultures, + UserCustomCulture = 8, + ReplacementCultures = 16, + WindowsOnlyCultures = 32, + FrameworkCultures = 64, + } +#endif public abstract class CultureInfo { @@ -168,26 +181,27 @@ public static CultureInfo InstalledUICulture } #endif -#if false - public DateTimeFormatInfo DateTimeFormat + public virtual DateTimeFormatInfo DateTimeFormat { get { Contract.Ensures(Contract.Result() != null); + return null; } set { Contract.Requires(value != null); } } -#endif -#if false - public CultureInfo Parent + public virtual CultureInfo Parent { - get; + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } } -#endif public virtual string EnglishName { @@ -225,14 +239,14 @@ public static CultureInfo ReadOnly(CultureInfo ci) public abstract object GetFormat(Type formatType); -#if false +#if !SILVERLIGHT + public static CultureInfo[] GetCultures(CultureTypes types) { + Contract.Ensures(Contract.Result() != null); return default(CultureInfo[]); } -#endif -#if !SILVERLIGHT public static CultureInfo CreateSpecificCulture(string name) { Contract.Ensures(Contract.Result() != null); diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs index 9d6197ca..a8d7c93d 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Globalization.DateTimeFormatInfo.cs @@ -170,6 +170,7 @@ public String[] AbbreviatedDayNames } } +#if !SILVERLIGHT public string DateSeparator { get @@ -183,6 +184,7 @@ public string DateSeparator Contract.Requires(value != null); } } +#endif public string FullDateTimePattern { @@ -198,6 +200,7 @@ public string FullDateTimePattern } } +#if !SILVERLIGHT public string TimeSeparator { get @@ -211,13 +214,13 @@ public string TimeSeparator Contract.Requires(value != null); } } - +#endif public Calendar Calendar { get { Contract.Ensures(Contract.Result() != null); - return default(string); + return default(Calendar); } set @@ -334,16 +337,20 @@ public string GetDayName(DayOfWeek dayofweek) return default(string); } + +#if !SILVERLIGHT public String[] GetAllDateTimePatterns(Char format) { - + Contract.Ensures(Contract.Result() != null); return default(String[]); } public String[] GetAllDateTimePatterns() { - + Contract.Ensures(Contract.Result() != null); return default(String[]); } +#endif + public string GetAbbreviatedDayName(DayOfWeek dayofweek) { Contract.Requires((int)dayofweek >= 0); @@ -369,24 +376,20 @@ public int GetEra(string eraName) return default(int); } - public object Clone() + public virtual object Clone() { return default(object); } - public object GetFormat(Type formatType) + public virtual object GetFormat(Type formatType) { return default(object); } public static DateTimeFormatInfo GetInstance(IFormatProvider provider) { - - return default(DateTimeFormatInfo); - } - public DateTimeFormatInfo() - { - return default(DateTimeFormatInfo); + Contract.Ensures(Contract.Result() != null); + return default(DateTimeFormatInfo); } } } diff --git a/Microsoft.Research/Contracts/MsCorlib/System.String.cs b/Microsoft.Research/Contracts/MsCorlib/System.String.cs index 85126c16..3157612b 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.String.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.String.cs @@ -162,6 +162,26 @@ public static String Concat(object arg0) Contract.Ensures(Contract.Result() != null); return default(String); } + +#if NETFRAMEWORK_4_0 || NETFRAMEWORK_4_5 + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static String Concat(IEnumerable args) + { + Contract.Ensures(Contract.Result() != null); + return default(String); + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static String Concat(IEnumerable args) + { + Contract.Ensures(Contract.Result() != null); + return default(String); + } +#endif + + [Pure] [Reads(ReadsAttribute.Reads.Nothing)] public static String Copy(String str) @@ -1198,6 +1218,17 @@ public static String Join(String separator, String[] value) } #if NETFRAMEWORK_4_0 || NETFRAMEWORK_4_5 + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static String Join(String separator, Object[] value) + { + Contract.Requires(value != null); + Contract.Ensures(Contract.Result() != null); + + return default(String); + } + [Pure] public static string Join(string separator, IEnumerable values) { diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Transform.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Transform.cs index 14e41792..e6aa6741 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Transform.cs +++ b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Transform.cs @@ -83,6 +83,7 @@ public static System.Windows.Media.Transform Identity { get { + Contract.Ensures(Contract.Result() != null); return default(System.Windows.Media.Transform); } } diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs index f50e4549..af92f926 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs +++ b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.Media.Visual.cs @@ -19,6 +19,7 @@ using System.Text; using System.Diagnostics.Contracts; using System; +using System.Windows.Media.Media3D; // Disable the "this variable is not used" warning as every field would imply it. #pragma warning disable 0414 @@ -104,21 +105,25 @@ int System.Windows.Media.Composition.DUCE.IResource.GetChannelCount() public GeneralTransform TransformToAncestor(System.Windows.Media.Visual ancestor) { + Contract.Ensures(Contract.Result() != null); return default(GeneralTransform); } public System.Windows.Media.Media3D.GeneralTransform2DTo3D TransformToAncestor(System.Windows.Media.Media3D.Visual3D ancestor) { + Contract.Ensures(Contract.Result() != null); return default(System.Windows.Media.Media3D.GeneralTransform2DTo3D); } public GeneralTransform TransformToDescendant(System.Windows.Media.Visual descendant) { + Contract.Ensures(Contract.Result() != null); return default(GeneralTransform); } public GeneralTransform TransformToVisual(System.Windows.Media.Visual visual) { + Contract.Ensures(Contract.Result() != null); return default(GeneralTransform); } diff --git a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.UIElement.cs b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.UIElement.cs index f6fa7f0d..750cbeda 100644 --- a/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.UIElement.cs +++ b/Microsoft.Research/Contracts/PresentationCore/Sources/System.Windows.UIElement.cs @@ -19,6 +19,7 @@ using System.Text; using System.Diagnostics.Contracts; using System; +using System.Windows.Input; // Disable the "this variable is not used" warning as every field would imply it. #pragma warning disable 0414 @@ -767,6 +768,7 @@ public System.Windows.Input.CommandBindingCollection CommandBindings { get { + Contract.Ensures(Contract.Result() != null); return default(System.Windows.Input.CommandBindingCollection); } } @@ -775,6 +777,7 @@ public Size DesiredSize { get { + Contract.Ensures(!Contract.Result().IsEmpty); return default(Size); } } @@ -813,6 +816,7 @@ public System.Windows.Input.InputBindingCollection InputBindings { get { + Contract.Ensures(Contract.Result() != null); return default(System.Windows.Input.InputBindingCollection); } } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Application.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Application.cs index 4bce84a4..b264b583 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Application.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Application.cs @@ -174,8 +174,7 @@ public static System.Windows.Application Current { get { - Contract.Ensures(Contract.Result() != null); - + // May return null if called from non-WPF application (e.g. WinForms app with embedded WPF controls). return default(System.Windows.Application); } } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Control.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Control.cs index ca793553..b9e1c76a 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Control.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Control.cs @@ -57,10 +57,12 @@ protected override System.Windows.Size MeasureOverride(System.Windows.Size const protected virtual new void OnMouseDoubleClick(System.Windows.Input.MouseButtonEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnPreviewMouseDoubleClick(System.Windows.Input.MouseButtonEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnTemplateChanged(ControlTemplate oldTemplate, ControlTemplate newTemplate) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Panel.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Panel.cs index abe56b1d..b9980394 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Panel.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.Panel.cs @@ -43,6 +43,7 @@ abstract public partial class Panel : System.Windows.FrameworkElement, System.Wi #region Methods and constructors protected virtual new UIElementCollection CreateUIElementCollection(System.Windows.FrameworkElement logicalParent) { + Contract.Ensures(Contract.Result() != null); return default(UIElementCollection); } @@ -106,10 +107,21 @@ public UIElementCollection Children { get { + Contract.Ensures(Contract.Result() != null); return default(UIElementCollection); } } + protected internal UIElementCollection InternalChildren + { + get + { + Contract.Ensures(Contract.Result() != null); + return default(UIElementCollection); + } + } + + internal protected virtual new bool HasLogicalOrientation { get diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TextBox.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TextBox.cs index 0b10e506..8495b588 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TextBox.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TextBox.cs @@ -282,6 +282,8 @@ public string Text { get { + // => TextBox.CoerceText will ensure value is never null. + Contract.Ensures(Contract.Result() != null); return default(string); } set diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.ToolTip.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.ToolTip.cs index 01286d29..8feb7193 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.ToolTip.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.ToolTip.cs @@ -43,6 +43,7 @@ public partial class ToolTip : ContentControl #region Methods and constructors protected virtual new void OnClosed(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } protected override System.Windows.Automation.Peers.AutomationPeer OnCreateAutomationPeer() @@ -52,6 +53,7 @@ protected override System.Windows.Automation.Peers.AutomationPeer OnCreateAutoma protected virtual new void OnOpened(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } protected override void OnVisualParentChanged(System.Windows.DependencyObject oldParent) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TreeViewItem.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TreeViewItem.cs index c4acfd19..e36dfaf6 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TreeViewItem.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.TreeViewItem.cs @@ -52,19 +52,23 @@ protected override System.Windows.DependencyObject GetContainerForItemOverride() protected virtual new void OnCollapsed(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnExpanded(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnSelected(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnUnselected(System.Windows.RoutedEventArgs e) { + Contract.Requires(e != null); } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingPanel.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingPanel.cs index d52ada7e..c26b6cf6 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingPanel.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingPanel.cs @@ -59,6 +59,7 @@ protected void InsertInternalChild(int index, System.Windows.UIElement child) protected virtual new void OnItemsChanged(Object sender, System.Windows.Controls.Primitives.ItemsChangedEventArgs args) { + Contract.Requires(args != null); } protected void RemoveInternalChildRange(int index, int range) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingStackPanel.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingStackPanel.cs index 60fedb00..5132e296 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingStackPanel.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Controls.VirtualizingStackPanel.cs @@ -1,295 +1,296 @@ -// 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. - -// File System.Windows.Controls.VirtualizingStackPanel.cs -// Automatically generated contract file. -using System.Collections.Generic; -using System.IO; -using System.Text; -using System.Diagnostics.Contracts; -using System; - -// Disable the "this variable is not used" warning as every field would imply it. -#pragma warning disable 0414 -// Disable the "this variable is never assigned to". -#pragma warning disable 0067 -// Disable the "this event is never assigned to". -#pragma warning disable 0649 -// Disable the "this variable is never used". -#pragma warning disable 0169 -// Disable the "new keyword not required" warning. -#pragma warning disable 0109 -// Disable the "extern without DllImport" warning. -#pragma warning disable 0626 -// Disable the "could hide other member" warning, can happen on certain properties. -#pragma warning disable 0108 - - -namespace System.Windows.Controls -{ - public partial class VirtualizingStackPanel : VirtualizingPanel, System.Windows.Controls.Primitives.IScrollInfo -#if NETFRAMEWORK_4_5 - , IStackMeasure -#endif - - { - #region Methods and constructors - public static void AddCleanUpVirtualizedItemHandler(System.Windows.DependencyObject element, CleanUpVirtualizedItemEventHandler handler) - { - } - - protected override System.Windows.Size ArrangeOverride(System.Windows.Size arrangeSize) - { - return default(System.Windows.Size); - } - - protected internal override void BringIndexIntoView(int index) - { - } - -#if !NETFRAMEWORK_4_5 - public static bool GetIsVirtualizing(System.Windows.DependencyObject o) - { - return default(bool); - } - - public static VirtualizationMode GetVirtualizationMode(System.Windows.DependencyObject element) - { - return default(VirtualizationMode); - } - - public static void SetIsVirtualizing(System.Windows.DependencyObject element, bool value) - { - } - - public static void SetVirtualizationMode(System.Windows.DependencyObject element, VirtualizationMode value) - { - } - - -#endif - - public virtual new void LineDown() - { - } - - public virtual new void LineLeft() - { - } - - public virtual new void LineRight() - { - } - - public virtual new void LineUp() - { - } - - public System.Windows.Rect MakeVisible(System.Windows.Media.Visual visual, System.Windows.Rect rectangle) - { - return default(System.Windows.Rect); - } - - protected override System.Windows.Size MeasureOverride(System.Windows.Size constraint) - { - return default(System.Windows.Size); - } - - public virtual new void MouseWheelDown() - { - } - - public virtual new void MouseWheelLeft() - { - } - - public virtual new void MouseWheelRight() - { - } - - public virtual new void MouseWheelUp() - { - } - - protected virtual new void OnCleanUpVirtualizedItem(CleanUpVirtualizedItemEventArgs e) - { - } - - protected override void OnClearChildren() - { - } - - protected override void OnItemsChanged(Object sender, System.Windows.Controls.Primitives.ItemsChangedEventArgs args) - { - } - - protected virtual new void OnViewportOffsetChanged(System.Windows.Vector oldViewportOffset, System.Windows.Vector newViewportOffset) - { - } - - protected virtual new void OnViewportSizeChanged(System.Windows.Size oldViewportSize, System.Windows.Size newViewportSize) - { - } - - public virtual new void PageDown() - { - } - - public virtual new void PageLeft() - { - } - - public virtual new void PageRight() - { - } - - public virtual new void PageUp() - { - } - - public static void RemoveCleanUpVirtualizedItemHandler(System.Windows.DependencyObject element, CleanUpVirtualizedItemEventHandler handler) - { - } - - public void SetHorizontalOffset(double offset) - { - } - - public void SetVerticalOffset(double offset) - { - } - - public VirtualizingStackPanel() - { - } - #endregion - - #region Properties and indexers - public bool CanHorizontallyScroll - { - get - { - return default(bool); - } - set - { - } - } - - public bool CanVerticallyScroll - { - get - { - return default(bool); - } - set - { - } - } - - public double ExtentHeight - { - get - { - return default(double); - } - } - - public double ExtentWidth - { - get - { - return default(double); - } - } - - internal protected override bool HasLogicalOrientation - { - get - { - return default(bool); - } - } - - public double HorizontalOffset - { - get - { - return default(double); - } - } - - internal protected override System.Windows.Controls.Orientation LogicalOrientation - { - get - { - return default(System.Windows.Controls.Orientation); - } - } - - public Orientation Orientation - { - get - { - return default(Orientation); - } - set - { - } - } - - public ScrollViewer ScrollOwner - { - get - { - return default(ScrollViewer); - } - set - { - } - } - - public double VerticalOffset - { - get - { - return default(double); - } - } - - public double ViewportHeight - { - get - { - return default(double); - } - } - - public double ViewportWidth - { - get - { - return default(double); - } - } - #endregion - - #region Fields - public readonly static System.Windows.RoutedEvent CleanUpVirtualizedItemEvent; - public readonly static System.Windows.DependencyProperty IsVirtualizingProperty; - public readonly static System.Windows.DependencyProperty OrientationProperty; - public readonly static System.Windows.DependencyProperty VirtualizationModeProperty; - #endregion - } -} +// 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. + +// File System.Windows.Controls.VirtualizingStackPanel.cs +// Automatically generated contract file. +using System.Collections.Generic; +using System.IO; +using System.Text; +using System.Diagnostics.Contracts; +using System; + +// Disable the "this variable is not used" warning as every field would imply it. +#pragma warning disable 0414 +// Disable the "this variable is never assigned to". +#pragma warning disable 0067 +// Disable the "this event is never assigned to". +#pragma warning disable 0649 +// Disable the "this variable is never used". +#pragma warning disable 0169 +// Disable the "new keyword not required" warning. +#pragma warning disable 0109 +// Disable the "extern without DllImport" warning. +#pragma warning disable 0626 +// Disable the "could hide other member" warning, can happen on certain properties. +#pragma warning disable 0108 + + +namespace System.Windows.Controls +{ + public partial class VirtualizingStackPanel : VirtualizingPanel, System.Windows.Controls.Primitives.IScrollInfo +#if NETFRAMEWORK_4_5 + , IStackMeasure +#endif + + { + #region Methods and constructors + public static void AddCleanUpVirtualizedItemHandler(System.Windows.DependencyObject element, CleanUpVirtualizedItemEventHandler handler) + { + } + + protected override System.Windows.Size ArrangeOverride(System.Windows.Size arrangeSize) + { + return default(System.Windows.Size); + } + + protected internal override void BringIndexIntoView(int index) + { + } + +#if !NETFRAMEWORK_4_5 + public static bool GetIsVirtualizing(System.Windows.DependencyObject o) + { + return default(bool); + } + + public static VirtualizationMode GetVirtualizationMode(System.Windows.DependencyObject element) + { + return default(VirtualizationMode); + } + + public static void SetIsVirtualizing(System.Windows.DependencyObject element, bool value) + { + } + + public static void SetVirtualizationMode(System.Windows.DependencyObject element, VirtualizationMode value) + { + } + + +#endif + + public virtual new void LineDown() + { + } + + public virtual new void LineLeft() + { + } + + public virtual new void LineRight() + { + } + + public virtual new void LineUp() + { + } + + public System.Windows.Rect MakeVisible(System.Windows.Media.Visual visual, System.Windows.Rect rectangle) + { + return default(System.Windows.Rect); + } + + protected override System.Windows.Size MeasureOverride(System.Windows.Size constraint) + { + return default(System.Windows.Size); + } + + public virtual new void MouseWheelDown() + { + } + + public virtual new void MouseWheelLeft() + { + } + + public virtual new void MouseWheelRight() + { + } + + public virtual new void MouseWheelUp() + { + } + + protected virtual new void OnCleanUpVirtualizedItem(CleanUpVirtualizedItemEventArgs e) + { + Contract.Requires(e != null); + } + + protected override void OnClearChildren() + { + } + + protected override void OnItemsChanged(Object sender, System.Windows.Controls.Primitives.ItemsChangedEventArgs args) + { + } + + protected virtual new void OnViewportOffsetChanged(System.Windows.Vector oldViewportOffset, System.Windows.Vector newViewportOffset) + { + } + + protected virtual new void OnViewportSizeChanged(System.Windows.Size oldViewportSize, System.Windows.Size newViewportSize) + { + } + + public virtual new void PageDown() + { + } + + public virtual new void PageLeft() + { + } + + public virtual new void PageRight() + { + } + + public virtual new void PageUp() + { + } + + public static void RemoveCleanUpVirtualizedItemHandler(System.Windows.DependencyObject element, CleanUpVirtualizedItemEventHandler handler) + { + } + + public void SetHorizontalOffset(double offset) + { + } + + public void SetVerticalOffset(double offset) + { + } + + public VirtualizingStackPanel() + { + } + #endregion + + #region Properties and indexers + public bool CanHorizontallyScroll + { + get + { + return default(bool); + } + set + { + } + } + + public bool CanVerticallyScroll + { + get + { + return default(bool); + } + set + { + } + } + + public double ExtentHeight + { + get + { + return default(double); + } + } + + public double ExtentWidth + { + get + { + return default(double); + } + } + + internal protected override bool HasLogicalOrientation + { + get + { + return default(bool); + } + } + + public double HorizontalOffset + { + get + { + return default(double); + } + } + + internal protected override System.Windows.Controls.Orientation LogicalOrientation + { + get + { + return default(System.Windows.Controls.Orientation); + } + } + + public Orientation Orientation + { + get + { + return default(Orientation); + } + set + { + } + } + + public ScrollViewer ScrollOwner + { + get + { + return default(ScrollViewer); + } + set + { + } + } + + public double VerticalOffset + { + get + { + return default(double); + } + } + + public double ViewportHeight + { + get + { + return default(double); + } + } + + public double ViewportWidth + { + get + { + return default(double); + } + } + #endregion + + #region Fields + public readonly static System.Windows.RoutedEvent CleanUpVirtualizedItemEvent; + public readonly static System.Windows.DependencyProperty IsVirtualizingProperty; + public readonly static System.Windows.DependencyProperty OrientationProperty; + public readonly static System.Windows.DependencyProperty VirtualizationModeProperty; + #endregion + } +} diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionContainer.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionContainer.cs index 42833ef2..e4665dad 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionContainer.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionContainer.cs @@ -47,10 +47,12 @@ public CollectionContainer() protected virtual new void OnContainedCollectionChanged(System.Collections.Specialized.NotifyCollectionChangedEventArgs args) { + Contract.Requires(args != null); } protected virtual new bool ReceiveWeakEvent(Type managerType, Object sender, EventArgs e) { + Contract.Requires(e != null); return default(bool); } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionView.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionView.cs index 699d7df6..317fa23a 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionView.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionView.cs @@ -112,10 +112,12 @@ protected bool OKToChangeCurrent() protected virtual new void OnBeginChangeLogging(System.Collections.Specialized.NotifyCollectionChangedEventArgs args) { + Contract.Requires(args != null); } protected virtual new void OnCollectionChanged(System.Collections.Specialized.NotifyCollectionChangedEventArgs args) { + Contract.Requires(args != null); } protected void OnCollectionChanged(Object sender, System.Collections.Specialized.NotifyCollectionChangedEventArgs args) @@ -128,6 +130,7 @@ protected void OnCollectionChanged(Object sender, System.Collections.Specialized protected virtual new void OnCurrentChanging(System.ComponentModel.CurrentChangingEventArgs args) { + Contract.Requires(args != null); } protected void OnCurrentChanging() @@ -136,6 +139,7 @@ protected void OnCurrentChanging() protected virtual new void OnPropertyChanged(System.ComponentModel.PropertyChangedEventArgs e) { + Contract.Requires(e != null); } public virtual new bool PassesFilter(Object item) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewGroup.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewGroup.cs index e4e7bed1..f8cd4d69 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewGroup.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewGroup.cs @@ -47,6 +47,7 @@ protected CollectionViewGroup(Object name) protected virtual new void OnPropertyChanged(System.ComponentModel.PropertyChangedEventArgs e) { + Contract.Requires(e != null); } #endregion diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewSource.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewSource.cs index 121098a6..878a5676 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewSource.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CollectionViewSource.cs @@ -15,6 +15,8 @@ // File System.Windows.Data.CollectionViewSource.cs // Automatically generated contract file. using System.Collections.Generic; +using System.Collections.ObjectModel; +using System.ComponentModel; using System.IO; using System.Text; using System.Diagnostics.Contracts; @@ -72,6 +74,7 @@ public static bool IsDefaultView(System.ComponentModel.ICollectionView view) protected virtual new bool ReceiveWeakEvent(Type managerType, Object sender, EventArgs e) { + Contract.Requires(e != null); return default(bool); } @@ -116,6 +119,7 @@ public System.Collections.ObjectModel.ObservableCollection>() != null); return default(System.Collections.ObjectModel.ObservableCollection); } } @@ -124,6 +128,7 @@ public System.ComponentModel.SortDescriptionCollection SortDescriptions { get { + Contract.Ensures(Contract.Result() != null); return default(System.ComponentModel.SortDescriptionCollection); } } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CompositeCollection.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CompositeCollection.cs index c9ffc002..fad36c43 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CompositeCollection.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Data.CompositeCollection.cs @@ -79,6 +79,7 @@ public void Insert(int insertIndex, Object insertItem) protected virtual new bool ReceiveWeakEvent(Type managerType, Object sender, EventArgs e) { + Contract.Requires(e != null); return default(bool); } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkContentElement.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkContentElement.cs index 4accd98c..6daa8ae8 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkContentElement.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkContentElement.cs @@ -102,10 +102,12 @@ public sealed override bool MoveFocus(System.Windows.Input.TraversalRequest requ protected virtual new void OnContextMenuClosing(System.Windows.Controls.ContextMenuEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnContextMenuOpening(System.Windows.Controls.ContextMenuEventArgs e) { + Contract.Requires(e != null); } protected override void OnGotFocus(RoutedEventArgs e) @@ -114,6 +116,7 @@ protected override void OnGotFocus(RoutedEventArgs e) protected virtual new void OnInitialized(EventArgs e) { + Contract.Requires(e != null); } protected override void OnPropertyChanged(DependencyPropertyChangedEventArgs e) @@ -126,10 +129,12 @@ protected override void OnPropertyChanged(DependencyPropertyChangedEventArgs e) protected virtual new void OnToolTipClosing(System.Windows.Controls.ToolTipEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnToolTipOpening(System.Windows.Controls.ToolTipEventArgs e) { + Contract.Requires(e != null); } public sealed override DependencyObject PredictFocus(System.Windows.Input.FocusNavigationDirection direction) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkElement.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkElement.cs index 30bbb272..10c4b0ee 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkElement.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.FrameworkElement.cs @@ -54,8 +54,32 @@ protected sealed override void ArrangeCore(Rect finalRect) { } - protected virtual new Size ArrangeOverride(Size finalSize) - { + /// + /// ArrangeOverride allows for the customization of the positioning of children. + /// + /// The final size that element should use to arrange itself and its children. + /// The size that element actually is going to use for rendering. If this size is not the same as finalSize + /// input parameter, the AlignmentX/AlignmentY properties will position the ink rect of the element + /// appropriately. + protected virtual Size ArrangeOverride(Size finalSize) + { + // Only a positive number is allowed here for width and height, since this will be used as the size of a physical Rect. + // See also comments or implementation of UIElement.Arrange() + Contract.Requires(!finalSize.IsEmpty + && !double.IsNaN(finalSize.Width) && !double.IsNaN(finalSize.Height) + && !double.IsPositiveInfinity(finalSize.Width) && !double.IsPositiveInfinity(finalSize.Height)); + + /* The function must return a physical size, i.e. positive numbers for Width and Height, so this would be the correct result contract: + * + * Contract.Ensures(!Contract.Result().IsEmpty + * && !double.IsNaN(Contract.Result().Width) && !double.IsNaN(Contract.Result().Height) + * && !double.IsInfinity(Contract.Result().Width) && !double.IsInfinity(Contract.Result().Height)); + * + * However in practice this is unusable; the analyzer can't infer all double operations in the method, + * because there are usually complex calculations, and we would end up with always the same huge Contract.Assume at the end, just + * to make the analyzer happy. + */ + return default(Size); } @@ -138,8 +162,29 @@ protected sealed override Size MeasureCore(Size availableSize) return default(Size); } - protected virtual new Size MeasureOverride(Size availableSize) - { + /// + /// Measurement override. Implement your size-to-content logic here. + /// + /// Available size that parent can give to the child. May be infinity (when parent wants to + /// measure to content). This is soft constraint. Child can return bigger size to indicate that it wants bigger space and hope + /// that parent can throw in scrolling... + /// Desired Size of the control, given available size passed as parameter. + protected virtual Size MeasureOverride(Size availableSize) + { + // Only positive number or positive infinity is allowed here for width and height, see also comments on UIElement.Measure. + Contract.Requires(!availableSize.IsEmpty && !double.IsNaN(availableSize.Width) && !double.IsNaN(availableSize.Height)); + + /* The function must return a physical size, i.e. positive numbers for Width and Height, so this would be the correct result contract: + * + * Contract.Ensures(!Contract.Result().IsEmpty + * && !double.IsNaN(Contract.Result().Width) && !double.IsNaN(Contract.Result().Height) + * && !double.IsInfinity(Contract.Result().Width) && !double.IsInfinity(Contract.Result().Height)); + * + * However in practice this is unusable; the analyzer can't infer all double operations in the method, + * because there are usually complex calculations, and we would end up with always the same huge Contract.Assume at the end, just + * to make the analyzer happy. + */ + return default(Size); } @@ -154,10 +199,12 @@ public sealed override bool MoveFocus(System.Windows.Input.TraversalRequest requ protected virtual new void OnContextMenuClosing(System.Windows.Controls.ContextMenuEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnContextMenuOpening(System.Windows.Controls.ContextMenuEventArgs e) { + Contract.Requires(e != null); } protected override void OnGotFocus(RoutedEventArgs e) @@ -166,6 +213,7 @@ protected override void OnGotFocus(RoutedEventArgs e) protected virtual new void OnInitialized(EventArgs e) { + Contract.Requires(e != null); } protected override void OnPropertyChanged(DependencyPropertyChangedEventArgs e) @@ -182,10 +230,12 @@ protected override void OnRenderSizeChanged(SizeChangedInfo sizeInfo) protected virtual new void OnToolTipClosing(System.Windows.Controls.ToolTipEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnToolTipOpening(System.Windows.Controls.ToolTipEventArgs e) { + Contract.Requires(e != null); } protected override void OnVisualParentChanged(DependencyObject oldParent) @@ -264,7 +314,7 @@ public double ActualHeight { get { - Contract.Ensures(Contract.Result() == this.RenderSize.Height); + Contract.Ensures(Contract.Result() >= 0.0); return default(double); } @@ -274,7 +324,7 @@ public double ActualWidth { get { - Contract.Ensures(Contract.Result() == this.RenderSize.Width); + Contract.Ensures(Contract.Result() >= 0.0); return default(double); } diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Interop.HwndHost.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Interop.HwndHost.cs index 91a4cd93..3ba66c2d 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Interop.HwndHost.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Interop.HwndHost.cs @@ -74,10 +74,12 @@ protected override System.Windows.Automation.Peers.AutomationPeer OnCreateAutoma protected override void OnKeyDown(System.Windows.Input.KeyEventArgs e) { + Contract.Requires(e != null); } protected override void OnKeyUp(System.Windows.Input.KeyEventArgs e) { + Contract.Requires(e != null); } protected virtual new bool OnMnemonicCore(ref MSG msg, System.Windows.Input.ModifierKeys modifiers) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.Localizer.BamlLocalizer.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.Localizer.BamlLocalizer.cs index 24283fd4..8d85fc4f 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.Localizer.BamlLocalizer.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Markup.Localizer.BamlLocalizer.cs @@ -62,6 +62,7 @@ public BamlLocalizationDictionary ExtractResources() protected virtual new void OnErrorNotify(BamlLocalizerErrorNotifyEventArgs e) { + Contract.Requires(e != null); } public void UpdateBaml(Stream target, BamlLocalizationDictionary updates) diff --git a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Window.cs b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Window.cs index 372a9506..6bc57217 100644 --- a/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Window.cs +++ b/Microsoft.Research/Contracts/PresentationFramework/Sources/System.Windows.Window.cs @@ -75,14 +75,17 @@ protected override Size MeasureOverride(Size availableSize) protected virtual new void OnActivated(EventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnClosed(EventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnClosing(System.ComponentModel.CancelEventArgs e) { + Contract.Requires(e != null); } protected override void OnContentChanged(Object oldContent, Object newContent) @@ -91,6 +94,7 @@ protected override void OnContentChanged(Object oldContent, Object newContent) protected virtual new void OnContentRendered(EventArgs e) { + Contract.Requires(e != null); } protected override System.Windows.Automation.Peers.AutomationPeer OnCreateAutomationPeer() @@ -100,10 +104,12 @@ protected override System.Windows.Automation.Peers.AutomationPeer OnCreateAutoma protected virtual new void OnDeactivated(EventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnLocationChanged(EventArgs e) { + Contract.Requires(e != null); } protected override void OnManipulationBoundaryFeedback(System.Windows.Input.ManipulationBoundaryFeedbackEventArgs e) @@ -112,10 +118,12 @@ protected override void OnManipulationBoundaryFeedback(System.Windows.Input.Mani protected virtual new void OnSourceInitialized(EventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnStateChanged(EventArgs e) { + Contract.Requires(e != null); } protected sealed override void OnVisualParentChanged(DependencyObject oldParent) diff --git a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.AggregateCatalog.cs b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.AggregateCatalog.cs index 8c59ce57..d205f499 100644 --- a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.AggregateCatalog.cs +++ b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.AggregateCatalog.cs @@ -64,10 +64,12 @@ protected override void Dispose(bool disposing) protected virtual new void OnChanged(ComposablePartCatalogChangeEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnChanging(ComposablePartCatalogChangeEventArgs e) { + Contract.Requires(e != null); } #endregion diff --git a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.DirectoryCatalog.cs b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.DirectoryCatalog.cs index 82a35292..7dbb4d0e 100644 --- a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.DirectoryCatalog.cs +++ b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.DirectoryCatalog.cs @@ -63,10 +63,12 @@ protected override void Dispose(bool disposing) protected virtual new void OnChanged(ComposablePartCatalogChangeEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnChanging(ComposablePartCatalogChangeEventArgs e) { + Contract.Requires(e != null); } public void Refresh() diff --git a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.ExportProvider.cs b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.ExportProvider.cs index 519b9c60..0b6fe58a 100644 --- a/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.ExportProvider.cs +++ b/Microsoft.Research/Contracts/System.ComponentModel.Composition/Sources/System.ComponentModel.Composition.Hosting.ExportProvider.cs @@ -67,12 +67,16 @@ public Lazy GetExport(string contractName) public T GetExportedValue(string contractName) { + Contract.Ensures(Contract.Result() != null); + // because of ImportCardinality.ExactlyOne => + // return this.GetExportedValueCore(contractName, ImportCardinality.ExactlyOne); return default(T); } public T GetExportedValue() { - return default(T); + Contract.Ensures(Contract.Result() != null); + return this.GetExportedValue((string)null); } public T GetExportedValueOrDefault() @@ -148,10 +152,12 @@ public IEnumerable> GetExports(Type type, Type metadataView protected virtual new void OnExportsChanged(ExportsChangeEventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnExportsChanging(ExportsChangeEventArgs e) { + Contract.Requires(e != null); } public bool TryGetExports(System.ComponentModel.Composition.Primitives.ImportDefinition definition, AtomicComposition atomicComposition, out IEnumerable exports) diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Enumerable.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Enumerable.cs index b5b42415..4746ea3c 100644 --- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Enumerable.cs +++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Enumerable.cs @@ -252,6 +252,7 @@ public static IEnumerable DefaultIfEmpty(this IEnumerable>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(IEnumerable); } @@ -279,6 +280,7 @@ public static IEnumerable DefaultIfEmpty(this IEnumerable>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(IEnumerable); } // diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs index 18469db0..0b1ea971 100644 --- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs +++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs @@ -5566,8 +5566,14 @@ public sealed class Expression { private Expression() { } - // public TDelegate Compile(); - } +#if !SILVERLIGHT + public TDelegate Compile() + { + Contract.Ensures(!ReferenceEquals(Contract.Result(), null)); + return default(TDelegate); + } +#endif + } } diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.ParallelEnumerable.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.ParallelEnumerable.cs index 01d0da88..e7b53a25 100644 --- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.ParallelEnumerable.cs +++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.ParallelEnumerable.cs @@ -406,6 +406,7 @@ public static ParallelQuery DefaultIfEmpty(ParallelQuery>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(ParallelQuery); } @@ -415,6 +416,7 @@ public static ParallelQuery DefaultIfEmpty(ParallelQuery>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(ParallelQuery); } diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Queryable.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Queryable.cs index c59cd7fc..14484f40 100644 --- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Queryable.cs +++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Queryable.cs @@ -926,6 +926,7 @@ public static IQueryable DefaultIfEmpty(this IQueryable>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(IQueryable); } // @@ -956,6 +957,7 @@ public static IQueryable DefaultIfEmpty(this IQueryable>() != null); + Contract.Ensures(Contract.Result>().Any()); return default(IQueryable); } // diff --git a/Microsoft.Research/Contracts/System.Data/System.Data.Common.DbConnectionStringBuilder.cs b/Microsoft.Research/Contracts/System.Data/System.Data.Common.DbConnectionStringBuilder.cs index 8c3700ce..88d35948 100644 --- a/Microsoft.Research/Contracts/System.Data/System.Data.Common.DbConnectionStringBuilder.cs +++ b/Microsoft.Research/Contracts/System.Data/System.Data.Common.DbConnectionStringBuilder.cs @@ -45,7 +45,14 @@ public string ConnectionString { extern public virtual bool IsFixedSize { get; } extern public virtual bool IsReadOnly { get; } - // Exceptions: + + // Property Value + // The value associated with the specified key. If the specified key is not found, + // trying to get it returns a null reference (Nothing in Visual Basic), and trying to set it creates a new element using the specified key. + // Passing a null (Nothing in Visual Basic) key throws an ArgumentNullException. + // Assigning a null value removes the key/value pair. + // + // Exceptions: // System.ArgumentNullException: // keyword is a null reference (Nothing in Visual Basic). // @@ -57,13 +64,11 @@ public virtual object this[string keyword] { get { - Contract.Ensures(Contract.Result() != null); return null; } - set { - Contract.Requires(value != null); + Contract.Requires(keyword != null); } } @@ -110,11 +115,18 @@ protected internal void ClearPropertyDescriptors() { } [Pure] protected virtual void GetProperties(Hashtable propertyDescriptors) { } - [Pure] - public virtual bool Remove(string keyword) { return false; } + public virtual bool Remove(string keyword) + { + Contract.Requires(keyword != null); + return false; + } [Pure] - public virtual bool ShouldSerialize(string keyword) { return false; } + public virtual bool ShouldSerialize(string keyword) + { + Contract.Requires(keyword != null); + return false; + } [Pure] public virtual bool TryGetValue(string keyword, out object value) diff --git a/Microsoft.Research/Contracts/System.Data/System.Data.DataRelation.cs b/Microsoft.Research/Contracts/System.Data/System.Data.DataRelation.cs index f5607f97..9f5bfb0e 100644 --- a/Microsoft.Research/Contracts/System.Data/System.Data.DataRelation.cs +++ b/Microsoft.Research/Contracts/System.Data/System.Data.DataRelation.cs @@ -13,6 +13,7 @@ // 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.Diagnostics.Contracts; namespace System.Data @@ -203,7 +204,15 @@ public class DataRelation // An array of System.Data.DataColumn objects. //[ResCategory("DataCategory_Data")] //[ResDescription("DataRelationChildColumnsDescr")] - //public virtual DataColumn[] ChildColumns { get; } + public virtual DataColumn[] ChildColumns + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } + // // Summary: // Gets the System.Data.ForeignKeyConstraint for the relation. diff --git a/Microsoft.Research/Contracts/System.Data/System.Data.DataRow.cs b/Microsoft.Research/Contracts/System.Data/System.Data.DataRow.cs index ba0652e6..55c013b9 100644 --- a/Microsoft.Research/Contracts/System.Data/System.Data.DataRow.cs +++ b/Microsoft.Research/Contracts/System.Data/System.Data.DataRow.cs @@ -98,7 +98,14 @@ public object[] ItemArray // // Returns: // The System.Data.DataTable to which this row belongs. - //public DataTable Table { get; } + public DataTable Table + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } // Summary: // Gets or sets the data stored in the specified System.Data.DataColumn. diff --git a/Microsoft.Research/Contracts/System.Data/System.Data.DataRowCollection.cs b/Microsoft.Research/Contracts/System.Data/System.Data.DataRowCollection.cs new file mode 100644 index 00000000..77eb2728 --- /dev/null +++ b/Microsoft.Research/Contracts/System.Data/System.Data.DataRowCollection.cs @@ -0,0 +1,220 @@ +// 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; +using System.Collections; + +namespace System.Data +{ + using System.Diagnostics.Contracts; + + /// + /// Represents a collection of rows for a . + /// + /// 1 + public sealed class DataRowCollection // : InternalDataCollectionBase + { + /// + /// Gets the total number of objects in this collection. + /// + /// + /// + /// The total number of objects in this collection. + /// + //public override int Count + //{ + // get + // { + // return 0; + // } + //} + + /// + /// Gets the row at the specified index. + /// + /// + /// + /// The specified . + /// + /// The zero-based index of the row to return. The index value is greater than the number of items in the collection. 1 + public DataRow this[int index] + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } + + /// + /// Adds the specified to the object. + /// + /// The to add. The row is null. The row either belongs to another table or already belongs to this table. The addition invalidates a constraint. The addition tries to put a null in a where is false 1 + public void Add(DataRow row) + { + Contract.Requires(row != null); + } + + /// + /// Inserts a new row into the collection at the specified location. + /// + /// The to add. The (zero-based) location in the collection where you want to add the DataRow. 1 + public void InsertAt(DataRow row, int pos) + { + Contract.Requires(row != null); + } + + /// + /// Gets the index of the specified object. + /// + /// + /// + /// The zero-based index of the row, or -1 if the row is not found in the collection. + /// + /// The DataRow to search for.1 + public int IndexOf(DataRow row) + { + Contract.Requires(row != null); + Contract.Ensures(Contract.Result() >= -1); + return 0; + } + + /// + /// Creates a row using specified values and adds it to the . + /// + /// + /// + /// None. + /// + /// The array of values that are used to create the new row. The array is larger than the number of columns in the table. A value does not match its respective column type. Adding the row invalidates a constraint. Trying to put a null in a column where is false. 1 + public DataRow Add(params object[] values) + { + Contract.Requires(values != null); + Contract.Ensures(Contract.Result() != null); + return null; + } + + /// + /// Gets the row specified by the primary key value. + /// + /// + /// + /// A that contains the primary key value specified; otherwise a null value if the primary key value does not exist in the . + /// + /// The primary key value of the to find. + /// The table does not have a primary key. + public DataRow Find(object key) + { + Contract.Requires(key != null); + return null; + } + + /// + /// Gets the row that contains the specified primary key values. + /// + /// + /// + /// A object that contains the primary key values specified; otherwise a null value if the primary key value does not exist in the . + /// + /// An array of primary key values to find. The type of the array is Object. + /// No row corresponds to that index value. + /// The table does not have a primary key. + public DataRow Find(object[] keys) + { + Contract.Requires(keys != null); + return null; + } + + /// + /// Clears the collection of all rows. + /// + /// A is enforced on the . 1 + public void Clear() + { + } + + /// + /// Gets a value that indicates whether the primary key of any row in the collection contains the specified value. + /// + /// + /// + /// true if the collection contains a with the specified primary key value; otherwise, false. + /// + /// The value of the primary key to test for. The table does not have a primary key. 1 + public bool Contains(object key) + { + Contract.Requires(key != null); + return false; + } + + /// + /// Gets a value that indicates whether the primary key columns of any row in the collection contain the values specified in the object array. + /// + /// + /// + /// true if the contains a with the specified key values; otherwise, false. + /// + /// An array of primary key values to test for. The table does not have a primary key. 1 + public bool Contains(object[] keys) + { + Contract.Requires(keys != null); + return false; + } + + /// + /// Copies all the objects from the collection into the given array, starting at the given destination array index. + /// + /// The one-dimensional array that is the destination of the elements copied from the DataRowCollection. The array must have zero-based indexing.The zero-based index in the array at which copying begins. + //public override void CopyTo(Array ar, int index) + //{ + //} + + /// + /// Copies all the objects from the collection into the given array, starting at the given destination array index. + /// + /// The one-dimensional array that is the destination of the elements copied from the DataRowCollection. The array must have zero-based indexing.The zero-based index in the array at which copying begins.2 + public void CopyTo(DataRow[] array, int index) + { + Contract.Requires(array != null); + } + + /// + /// Gets an for this collection. + /// + /// + /// + /// An for this collection. + /// + //public override IEnumerator GetEnumerator() + //{ + //} + + /// + /// Removes the specified from the collection. + /// + /// The to remove. 1 + public void Remove(DataRow row) + { + Contract.Requires(row != null); + } + + /// + /// Removes the row at the specified index from the collection. + /// + /// The index of the row to remove. 1 + public void RemoveAt(int index) + { + } + } +} diff --git a/Microsoft.Research/Contracts/System.Data/System.Data.DataTable.cs b/Microsoft.Research/Contracts/System.Data/System.Data.DataTable.cs index 1f33e214..b33969b5 100644 --- a/Microsoft.Research/Contracts/System.Data/System.Data.DataTable.cs +++ b/Microsoft.Research/Contracts/System.Data/System.Data.DataTable.cs @@ -329,7 +329,20 @@ public DataColumn[] PrimaryKey // otherwise a null value if no System.Data.DataRow objects exist. //[Browsable(false)] //[ResDescription("DataTableRowsDescr")] - //public DataRowCollection Rows { get; } + public DataRowCollection Rows + { + get + { + // Here the documentation is definitely wrong! + // + // internal readonly DataRowCollection rowCollection; + // + // return this.rowCollection; + + Contract.Ensures(Contract.Result() != null); + return null; + } + } // // Summary: // Gets or sets an System.ComponentModel.ISite for the System.Data.DataTable. diff --git a/Microsoft.Research/Contracts/System.Data/System.Data10.csproj b/Microsoft.Research/Contracts/System.Data/System.Data10.csproj index d035ae32..ad5a0c14 100644 --- a/Microsoft.Research/Contracts/System.Data/System.Data10.csproj +++ b/Microsoft.Research/Contracts/System.Data/System.Data10.csproj @@ -285,6 +285,9 @@ PreContractsBuildDummy + + + ..\$(OutputPath) diff --git a/Microsoft.Research/Contracts/System.Web.ApplicationServices/Sources/System.Web.Security.MembershipProvider.cs b/Microsoft.Research/Contracts/System.Web.ApplicationServices/Sources/System.Web.Security.MembershipProvider.cs index e39a4246..ae142e5e 100644 --- a/Microsoft.Research/Contracts/System.Web.ApplicationServices/Sources/System.Web.Security.MembershipProvider.cs +++ b/Microsoft.Research/Contracts/System.Web.ApplicationServices/Sources/System.Web.Security.MembershipProvider.cs @@ -86,6 +86,7 @@ protected MembershipProvider() protected virtual new void OnValidatingPassword(ValidatePasswordEventArgs e) { + Contract.Requires(e != null); } public abstract string ResetPassword(string username, string answer); diff --git a/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.BaseDataBoundControl.cs b/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.BaseDataBoundControl.cs index 0dbef215..f3e11019 100644 --- a/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.BaseDataBoundControl.cs +++ b/Microsoft.Research/Contracts/System.Web/System.Web.UI.WebControls.BaseDataBoundControl.cs @@ -57,6 +57,7 @@ public override void DataBind () protected virtual new void OnDataBound (EventArgs e) { + Contract.Requires(e != null); } protected virtual new void OnDataPropertyChanged () @@ -69,6 +70,7 @@ protected internal override void OnInit (EventArgs e) protected virtual new void OnPagePreLoad (Object sender, EventArgs e) { + Contract.Requires(e != null); } protected internal override void OnPreRender (EventArgs e) diff --git a/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq.XProcessingInstruction.cs b/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq.XProcessingInstruction.cs new file mode 100644 index 00000000..7ab3d768 --- /dev/null +++ b/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq.XProcessingInstruction.cs @@ -0,0 +1,75 @@ +// 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; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace System.Xml.Linq +{ + using System.Diagnostics.Contracts; + + public class XProcessingInstruction : XNode + { + public string Data + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + set + { + Contract.Requires(value != null); + } + } + + public override XmlNodeType NodeType + { + get + { + return XmlNodeType.ProcessingInstruction; + } + } + + public string Target + { + get + { + Contract.Ensures(!string.IsNullOrEmpty(Contract.Result())); + return null; + } + set + { + Contract.Requires(!string.IsNullOrEmpty(value)); + } + } + + public XProcessingInstruction(string target, string data) + { + Contract.Requires(!string.IsNullOrEmpty(target)); + Contract.Requires(data != null); + } + + public XProcessingInstruction(XProcessingInstruction other) + { + Contract.Requires(other != null); + } + + public override void WriteTo(XmlWriter writer) + { + } + } +} diff --git a/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq10.csproj b/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq10.csproj index 366433ca..e99ea13f 100644 --- a/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq10.csproj +++ b/Microsoft.Research/Contracts/System.Xml.Linq/System.Xml.Linq10.csproj @@ -202,6 +202,7 @@ + diff --git a/Microsoft.Research/Contracts/System/System.Collections.ObjectModel.ObservableCollection.cs b/Microsoft.Research/Contracts/System/System.Collections.ObjectModel.ObservableCollection.cs new file mode 100644 index 00000000..f9cee645 --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.Collections.ObjectModel.ObservableCollection.cs @@ -0,0 +1,193 @@ +using System; +using System.Collections.Generic; +using System.Collections.Specialized; +using System.ComponentModel; +using System.Diagnostics.Contracts; +using System.Runtime; +using System.Runtime.CompilerServices; + +namespace System.Collections.ObjectModel +{ +#if !SILVERLIGHT && !NETFRAMEWORK_3_5 // => types defined in WindowsBase! + // Summary: + // Represents a dynamic data collection that provides notifications when items + // get added, removed, or when the whole list is refreshed. + // + // Type parameters: + // T: + // The type of elements in the collection. + public class ObservableCollection : Collection, INotifyCollectionChanged, INotifyPropertyChanged + { + // Summary: + // Initializes a new instance of the System.Collections.ObjectModel.ObservableCollection + // class. + public ObservableCollection() { } + // + // Summary: + // Initializes a new instance of the System.Collections.ObjectModel.ObservableCollection + // class that contains elements copied from the specified collection. + // + // Parameters: + // collection: + // The collection from which the elements are copied. + // + // Exceptions: + // System.ArgumentNullException: + // The collection parameter cannot be null. + public ObservableCollection(IEnumerable collection) + { + Contract.Requires(collection != null); + } + + // + // Summary: + // Initializes a new instance of the System.Collections.ObjectModel.ObservableCollection + // class that contains elements copied from the specified list. + // + // Parameters: + // list: + // The list from which the elements are copied. + // + // Exceptions: + // System.ArgumentNullException: + // The list parameter cannot be null. + public ObservableCollection(List list) + { + Contract.Requires(list != null); + } + + public virtual event NotifyCollectionChangedEventHandler CollectionChanged + { + add + { + } + remove + { + } + } + + // + // Summary: + // Occurs when a property value changes. + //protected virtual event PropertyChangedEventHandler PropertyChanged; + + // Summary: + // Disallows reentrant attempts to change this collection. + // + // Returns: + // An System.IDisposable object that can be used to dispose of the object. + //protected IDisposable BlockReentrancy(); + // + // Summary: + // Checks for reentrant attempts to change this collection. + // + // Exceptions: + // System.InvalidOperationException: + // If there was a call to System.Collections.ObjectModel.ObservableCollection.BlockReentrancy() + // of which the System.IDisposable return value has not yet been disposed of. + // Typically, this means when there are additional attempts to change this collection + // during a System.Collections.ObjectModel.ObservableCollection.CollectionChanged + // event. However, it depends on when derived classes choose to call System.Collections.ObjectModel.ObservableCollection.BlockReentrancy(). + //protected void CheckReentrancy(); + // + // Summary: + // Removes all items from the collection. + protected override void ClearItems() + { + } + + // + // Summary: + // Inserts an item into the collection at the specified index. + // + // Parameters: + // index: + // The zero-based index at which item should be inserted. + // + // item: + // The object to insert. + protected override void InsertItem(int index, T item) + { + } + // + // Summary: + // Moves the item at the specified index to a new location in the collection. + // + // Parameters: + // oldIndex: + // The zero-based index specifying the location of the item to be moved. + // + // newIndex: + // The zero-based index specifying the new location of the item. + public void Move(int oldIndex, int newIndex) + { + Contract.Requires((oldIndex >= 0) && (oldIndex < Count)); + Contract.Requires((newIndex >= 0) && (newIndex < Count)); + } + // + // Summary: + // Moves the item at the specified index to a new location in the collection. + // + // Parameters: + // oldIndex: + // The zero-based index specifying the location of the item to be moved. + // + // newIndex: + // The zero-based index specifying the new location of the item. + protected virtual void MoveItem(int oldIndex, int newIndex) + { + Contract.Requires((oldIndex >= 0) && (oldIndex < Count)); + Contract.Requires((newIndex >= 0) && (newIndex < Count)); + } + // + // Summary: + // Raises the System.Collections.ObjectModel.ObservableCollection.CollectionChanged + // event with the provided arguments. + // + // Parameters: + // e: + // Arguments of the event being raised. + protected virtual void OnCollectionChanged(NotifyCollectionChangedEventArgs e) + { + Contract.Requires(e != null); + } + // + // Summary: + // Raises the System.Collections.ObjectModel.ObservableCollection.PropertyChanged + // event with the provided arguments. + // + // Parameters: + // e: + // Arguments of the event being raised. + protected virtual void OnPropertyChanged(PropertyChangedEventArgs e) + { + Contract.Requires(e != null); + } + // + // Summary: + // Removes the item at the specified index of the collection. + // + // Parameters: + // index: + // The zero-based index of the element to remove. + protected override void RemoveItem(int index) { } + // + // Summary: + // Replaces the element at the specified index. + // + // Parameters: + // index: + // The zero-based index of the element to replace. + // + // item: + // The new value for the element at the specified index. + protected override void SetItem(int index, T item) { } + + event PropertyChangedEventHandler INotifyPropertyChanged.PropertyChanged + { + add { throw new NotImplementedException(); } + remove { throw new NotImplementedException(); } + } + } +#endif +} diff --git a/Microsoft.Research/Contracts/System/System.Collections.Specialized.INotifyCollectionChanged.cs b/Microsoft.Research/Contracts/System/System.Collections.Specialized.INotifyCollectionChanged.cs new file mode 100644 index 00000000..96ac03e3 --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.Collections.Specialized.INotifyCollectionChanged.cs @@ -0,0 +1,359 @@ +using System.Runtime.CompilerServices; + +namespace System.Collections.Specialized +{ +#if !SILVERLIGHT && !NETFRAMEWORK_3_5 // => types defined in WindowsBase! + // Summary: + // Describes the action that caused a System.Collections.Specialized.INotifyCollectionChanged.CollectionChanged + // event. + public enum NotifyCollectionChangedAction + { + // Summary: + // One or more items were added to the collection. + Add = 0, + // + // Summary: + // One or more items were removed from the collection. + Remove = 1, + // + // Summary: + // One or more items were replaced in the collection. + Replace = 2, + // + // Summary: + // One or more items were moved within the collection. + Move = 3, + // + // Summary: + // The content of the collection changed dramatically. + Reset = 4, + } + + + // Summary: + // Provides data for the System.Collections.Specialized.INotifyCollectionChanged.CollectionChanged + // event. + public class NotifyCollectionChangedEventArgs : EventArgs + { + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a System.Collections.Specialized.NotifyCollectionChangedAction.Reset + // change. + // + // Parameters: + // action: + // The action that caused the event. This must be set to System.Collections.Specialized.NotifyCollectionChangedAction.Reset. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a multi-item change. + // + // Parameters: + // action: + // The action that caused the event. This can be set to System.Collections.Specialized.NotifyCollectionChangedAction.Reset, + // System.Collections.Specialized.NotifyCollectionChangedAction.Add, or System.Collections.Specialized.NotifyCollectionChangedAction.Remove. + // + // changedItems: + // The items that are affected by the change. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, IList changedItems) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a one-item change. + // + // Parameters: + // action: + // The action that caused the event. This can be set to System.Collections.Specialized.NotifyCollectionChangedAction.Reset, + // System.Collections.Specialized.NotifyCollectionChangedAction.Add, or System.Collections.Specialized.NotifyCollectionChangedAction.Remove. + // + // changedItem: + // The item that is affected by the change. + // + // Exceptions: + // System.ArgumentException: + // If action is not Reset, Add, or Remove, or if action is Reset and changedItem + // is not null. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, object changedItem) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a multi-item System.Collections.Specialized.NotifyCollectionChangedAction.Replace + // change. + // + // Parameters: + // action: + // The action that caused the event. This can only be set to System.Collections.Specialized.NotifyCollectionChangedAction.Replace. + // + // newItems: + // The new items that are replacing the original items. + // + // oldItems: + // The original items that are replaced. + // + // Exceptions: + // System.ArgumentException: + // If action is not Replace. + // + // System.ArgumentNullException: + // If oldItems or newItems is null. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, IList newItems, IList oldItems) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a multi-item change or a System.Collections.Specialized.NotifyCollectionChangedAction.Reset + // change. + // + // Parameters: + // action: + // The action that caused the event. This can be set to System.Collections.Specialized.NotifyCollectionChangedAction.Reset, + // System.Collections.Specialized.NotifyCollectionChangedAction.Add, or System.Collections.Specialized.NotifyCollectionChangedAction.Remove. + // + // changedItems: + // The items affected by the change. + // + // startingIndex: + // The index where the change occurred. + // + // Exceptions: + // System.ArgumentException: + // If action is not Reset, Add, or Remove, if action is Reset and either changedItems + // is not null or startingIndex is not -1, or if action is Add or Remove and + // startingIndex is less than -1. + // + // System.ArgumentNullException: + // If action is Add or Remove and changedItems is null. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, IList changedItems, int startingIndex) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a one-item change. + // + // Parameters: + // action: + // The action that caused the event. This can be set to System.Collections.Specialized.NotifyCollectionChangedAction.Reset, + // System.Collections.Specialized.NotifyCollectionChangedAction.Add, or System.Collections.Specialized.NotifyCollectionChangedAction.Remove. + // + // changedItem: + // The item that is affected by the change. + // + // index: + // The index where the change occurred. + // + // Exceptions: + // System.ArgumentException: + // If action is not Reset, Add, or Remove, or if action is Reset and either + // changedItems is not null or index is not -1. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, object changedItem, int index) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a one-item System.Collections.Specialized.NotifyCollectionChangedAction.Replace + // change. + // + // Parameters: + // action: + // The action that caused the event. This can only be set to System.Collections.Specialized.NotifyCollectionChangedAction.Replace. + // + // newItem: + // The new item that is replacing the original item. + // + // oldItem: + // The original item that is replaced. + // + // Exceptions: + // System.ArgumentException: + // If action is not Replace. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, object newItem, object oldItem) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a multi-item System.Collections.Specialized.NotifyCollectionChangedAction.Replace + // change. + // + // Parameters: + // action: + // The action that caused the event. This can only be set to System.Collections.Specialized.NotifyCollectionChangedAction.Replace. + // + // newItems: + // The new items that are replacing the original items. + // + // oldItems: + // The original items that are replaced. + // + // startingIndex: + // The index of the first item of the items that are being replaced. + // + // Exceptions: + // System.ArgumentException: + // If action is not Replace. + // + // System.ArgumentNullException: + // If oldItems or newItems is null. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, IList newItems, IList oldItems, int startingIndex) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a multi-item System.Collections.Specialized.NotifyCollectionChangedAction.Move + // change. + // + // Parameters: + // action: + // The action that caused the event. This can only be set to System.Collections.Specialized.NotifyCollectionChangedAction.Move. + // + // changedItems: + // The items affected by the change. + // + // index: + // The new index for the changed items. + // + // oldIndex: + // The old index for the changed items. + // + // Exceptions: + // System.ArgumentException: + // If action is not Move or index is less than 0. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, IList changedItems, int index, int oldIndex) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a one-item System.Collections.Specialized.NotifyCollectionChangedAction.Move + // change. + // + // Parameters: + // action: + // The action that caused the event. This can only be set to System.Collections.Specialized.NotifyCollectionChangedAction.Move. + // + // changedItem: + // The item affected by the change. + // + // index: + // The new index for the changed item. + // + // oldIndex: + // The old index for the changed item. + // + // Exceptions: + // System.ArgumentException: + // If action is not Move or index is less than 0. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, object changedItem, int index, int oldIndex) { } + // + // Summary: + // Initializes a new instance of the System.Collections.Specialized.NotifyCollectionChangedEventArgs + // class that describes a one-item System.Collections.Specialized.NotifyCollectionChangedAction.Replace + // change. + // + // Parameters: + // action: + // The action that caused the event. This can be set to System.Collections.Specialized.NotifyCollectionChangedAction.Replace. + // + // newItem: + // The new item that is replacing the original item. + // + // oldItem: + // The original item that is replaced. + // + // index: + // The index of the item being replaced. + // + // Exceptions: + // System.ArgumentException: + // If action is not Replace. + public NotifyCollectionChangedEventArgs(NotifyCollectionChangedAction action, object newItem, object oldItem, int index) { } + + // Summary: + // Gets the action that caused the event. + // + // Returns: + // A System.Collections.Specialized.NotifyCollectionChangedAction value that + // describes the action that caused the event. + public NotifyCollectionChangedAction Action + { + get + { + return default(NotifyCollectionChangedAction); + } + } + // + // Summary: + // Gets the list of new items involved in the change. + // + // Returns: + // The list of new items involved in the change. + public IList NewItems + { + get + { + return null; + } + } + + // + // Summary: + // Gets the index at which the change occurred. + // + // Returns: + // The zero-based index at which the change occurred. + public int NewStartingIndex + { + get + { + return 0; + } + + } + // + // Summary: + // Gets the list of items affected by a System.Collections.Specialized.NotifyCollectionChangedAction.Replace, + // Remove, or Move action. + // + // Returns: + // The list of items affected by a System.Collections.Specialized.NotifyCollectionChangedAction.Replace, + // Remove, or Move action. + public IList OldItems + { + get + { + return null; + } + } + // + // Summary: + // Gets the index at which a System.Collections.Specialized.NotifyCollectionChangedAction.Move, + // Remove, or Replace action occurred. + // + // Returns: + // The zero-based index at which a System.Collections.Specialized.NotifyCollectionChangedAction.Move, + // Remove, or Replace action occurred. + public int OldStartingIndex + { + get + { + return 0; + } + } + } + + // Summary: + // Represents the method that handles the System.Collections.Specialized.INotifyCollectionChanged.CollectionChanged + // event. + // + // Parameters: + // sender: + // The object that raised the event. + // + // e: + // Information about the event. + public delegate void NotifyCollectionChangedEventHandler(object sender, NotifyCollectionChangedEventArgs e); + + // Summary: + // Notifies listeners of dynamic changes, such as when items get added and removed + // or the whole list is refreshed. + public interface INotifyCollectionChanged + { + // Summary: + // Occurs when the collection changes. + event NotifyCollectionChangedEventHandler CollectionChanged; + } +#endif +} diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.INotifyPropertyChanged.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.INotifyPropertyChanged.cs new file mode 100644 index 00000000..cb891301 --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.INotifyPropertyChanged.cs @@ -0,0 +1,11 @@ +namespace System.ComponentModel +{ + // Summary: + // Notifies clients that a property value has changed. + public interface INotifyPropertyChanged + { + // Summary: + // Occurs when a property value changes. + event PropertyChangedEventHandler PropertyChanged; + } +} diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventArgs.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventArgs.cs new file mode 100644 index 00000000..2776ed0c --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventArgs.cs @@ -0,0 +1,28 @@ +namespace System.ComponentModel +{ + using System; + using System.Diagnostics.Contracts; + + public class PropertyChangedEventArgs : EventArgs + { + public PropertyChangedEventArgs(string propertyName) + { + Contract.Requires(!string.IsNullOrEmpty(Contract.Result())); + Contract.Ensures(this.PropertyName == propertyName); + } + +#if SILVERLIGHT + public string PropertyName +#else + public virtual string PropertyName +#endif + { + get + { + Contract.Ensures(!string.IsNullOrEmpty(Contract.Result())); + + return default(string); + } + } + } +} diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventHandler.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventHandler.cs new file mode 100644 index 00000000..38d0c148 --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyChangedEventHandler.cs @@ -0,0 +1,4 @@ +namespace System.ComponentModel +{ + public delegate void PropertyChangedEventHandler(Object sender, PropertyChangedEventArgs e); +} diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs index 06f6ba55..51c55a43 100644 --- a/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.PropertyDescriptor.cs @@ -182,7 +182,6 @@ protected object CreateInstance(Type type) return default(object); } -#endif // // Summary: // Compares this to another object to see if they are equivalent. @@ -333,9 +332,11 @@ protected object CreateInstance(Type type) // // e: // An System.EventArgs that contains the event data. - //protected virtual void OnValueChanged(object component, EventArgs e); + protected virtual void OnValueChanged(object component, EventArgs e) + { + Contract.Requires(e != null); + } -#if !SILVERLIGHT // // Summary: // Enables other objects to be notified when this property changes. diff --git a/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs b/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs index c8a56a15..1b974e92 100644 --- a/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs +++ b/Microsoft.Research/Contracts/System/System.ComponentModel.TypeDescriptor.cs @@ -589,6 +589,7 @@ public static string GetComponentName(object component, bool noCustomTypeDesc) public static TypeConverter GetConverter(object component) { Contract.Requires(component != null); + Contract.Ensures(Contract.Result() != null); return default(TypeConverter); } @@ -609,6 +610,7 @@ public static TypeConverter GetConverter(object component) public static TypeConverter GetConverter(Type type) { Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); return default(TypeConverter); } @@ -638,6 +640,7 @@ public static TypeConverter GetConverter(Type type) public static TypeConverter GetConverter(object component, bool noCustomTypeDesc) { Contract.Requires(component != null); + Contract.Ensures(Contract.Result() != null); return default(TypeConverter); } diff --git a/Microsoft.Research/Contracts/System/System.Contracts10.csproj b/Microsoft.Research/Contracts/System/System.Contracts10.csproj index 10e44f0c..596dd440 100644 --- a/Microsoft.Research/Contracts/System/System.Contracts10.csproj +++ b/Microsoft.Research/Contracts/System/System.Contracts10.csproj @@ -561,6 +561,11 @@ AssemblyInfo.cs + + + + + @@ -706,6 +711,9 @@ PreContractsBuildDummy + + + ..\$(OutputPath) diff --git a/Microsoft.Research/Contracts/System/System.Diagnostics.FileVersionInfo.cs b/Microsoft.Research/Contracts/System/System.Diagnostics.FileVersionInfo.cs new file mode 100644 index 00000000..4282accb --- /dev/null +++ b/Microsoft.Research/Contracts/System/System.Diagnostics.FileVersionInfo.cs @@ -0,0 +1,36 @@ + + +// 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.Diagnostics.Contracts; +using System; + +namespace System.Diagnostics +{ +#if !SILVERLIGHT + public sealed class FileVersionInfo + { + private FileVersionInfo() + { + } + + public static FileVersionInfo GetVersionInfo(string fileName) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } +#endif +} diff --git a/Microsoft.Research/Contracts/System/System.Diagnostics.TraceListener.cs b/Microsoft.Research/Contracts/System/System.Diagnostics.TraceListener.cs index 207d51ee..16c4d81c 100644 --- a/Microsoft.Research/Contracts/System/System.Diagnostics.TraceListener.cs +++ b/Microsoft.Research/Contracts/System/System.Diagnostics.TraceListener.cs @@ -13,7 +13,7 @@ // 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 !SILVERLIGHT - +using System.Collections.Specialized; using System.Diagnostics.Contracts; using System; @@ -48,6 +48,15 @@ public int IndentSize } } + public StringDictionary Attributes + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } + #if false public void WriteLine (object o, string category) { diff --git a/Microsoft.Research/Contracts/System/System.Diagnostics.TraceSource.cs b/Microsoft.Research/Contracts/System/System.Diagnostics.TraceSource.cs index add41747..b8b56385 100644 --- a/Microsoft.Research/Contracts/System/System.Diagnostics.TraceSource.cs +++ b/Microsoft.Research/Contracts/System/System.Diagnostics.TraceSource.cs @@ -16,6 +16,7 @@ using System; using System.Runtime; using System.Diagnostics.Contracts; +using System.Collections.Specialized; namespace System.Diagnostics { @@ -35,7 +36,7 @@ public TraceSource(string name, SourceLevels defaultLevel) } - /* + public StringDictionary Attributes { get @@ -55,7 +56,7 @@ public TraceListenerCollection Listeners return null; } } - */ + public string Name { get { Contract.Ensures(Contract.Result() != null); return null; } } diff --git a/Microsoft.Research/Contracts/System/System.Net.WebRequest.cs b/Microsoft.Research/Contracts/System/System.Net.WebRequest.cs index 2052d486..d073affc 100644 --- a/Microsoft.Research/Contracts/System/System.Net.WebRequest.cs +++ b/Microsoft.Research/Contracts/System/System.Net.WebRequest.cs @@ -169,7 +169,17 @@ public static IWebProxy DefaultWebProxy // System.NotImplementedException: // Any attempt is made to get or set the property, when the property is not // overridden in a descendant class. - // public virtual WebHeaderCollection Headers { get; set; } + public virtual WebHeaderCollection Headers + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + set + { + } + } // // Summary: @@ -190,7 +200,18 @@ public static IWebProxy DefaultWebProxy // System.NotImplementedException: // If the property is not overridden in a descendant class, any attempt is made // to get or set the property. - extern public virtual string Method { get; set; } + public virtual string Method + { + get + { + Contract.Ensures(!String.IsNullOrEmpty(Contract.Result())); + return null; + } + set + { + Contract.Requires(!String.IsNullOrEmpty(value)); + } + } // // Summary: // When overridden in a descendant class, indicates whether to pre-authenticate @@ -220,7 +241,7 @@ public virtual IWebProxy Proxy { get { - Contract.Ensures(Contract.Result() != null); + // default is not null, but it's possible to set proxy to null. return default(IWebProxy); } set @@ -297,7 +318,11 @@ public virtual IWebProxy Proxy // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual IAsyncResult BeginGetRequestStream(AsyncCallback callback, object state); + public virtual IAsyncResult BeginGetRequestStream(AsyncCallback callback, object state) + { + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // When overridden in a descendant class, begins an asynchronous request for @@ -317,7 +342,11 @@ public virtual IWebProxy Proxy // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual IAsyncResult BeginGetResponse(AsyncCallback callback, object state); + public virtual IAsyncResult BeginGetResponse(AsyncCallback callback, object state) + { + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // Initializes a new System.Net.WebRequest instance for the specified URI scheme. @@ -345,6 +374,7 @@ public virtual IWebProxy Proxy public static WebRequest Create(string requestUriString) { Contract.Requires(requestUriString != null); + Contract.Ensures(Contract.Result() != null); return default(WebRequest); } @@ -372,6 +402,7 @@ public static WebRequest Create(string requestUriString) public static WebRequest Create(Uri requestUri) { Contract.Requires(requestUri != null); + Contract.Ensures(Contract.Result() != null); return default(WebRequest); } @@ -399,6 +430,7 @@ public static WebRequest Create(Uri requestUri) public static WebRequest CreateDefault(Uri requestUri) { Contract.Requires(requestUri != null); + Contract.Ensures(Contract.Result() != null); return default(WebRequest); } @@ -418,7 +450,12 @@ public static WebRequest CreateDefault(Uri requestUri) // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual Stream EndGetRequestStream(IAsyncResult asyncResult); + public virtual Stream EndGetRequestStream(IAsyncResult asyncResult) + { + Contract.Requires(asyncResult != null); + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // When overridden in a descendant class, returns a System.Net.WebResponse. @@ -434,7 +471,12 @@ public static WebRequest CreateDefault(Uri requestUri) // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual WebResponse EndGetResponse(IAsyncResult asyncResult); + public virtual WebResponse EndGetResponse(IAsyncResult asyncResult) + { + Contract.Requires(asyncResult != null); + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // Populates a System.Runtime.Serialization.SerializationInfo with the data @@ -460,7 +502,11 @@ public static WebRequest CreateDefault(Uri requestUri) // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual Stream GetRequestStream(); + public virtual Stream GetRequestStream() + { + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // When overridden in a descendant class, returns a response to an Internet @@ -473,7 +519,11 @@ public static WebRequest CreateDefault(Uri requestUri) // System.NotImplementedException: // Any attempt is made to access the method, when the method is not overridden // in a descendant class. - //public virtual WebResponse GetResponse(); + public virtual WebResponse GetResponse() + { + Contract.Ensures(Contract.Result() != null); + return null; + } // // Summary: // Returns a proxy configured with the Internet Explorer settings of the currently diff --git a/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresTest.cs b/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresTest.cs new file mode 100644 index 00000000..ada9d6e0 --- /dev/null +++ b/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresTest.cs @@ -0,0 +1,107 @@ +namespace SystemRequiresVerificationTests +{ + using System; + using System.Windows; + + using Microsoft.VisualStudio.TestTools.UnitTesting; + + [TestClass] + public class SystemRequiresTest + { + [TestMethod] + public void Rect_ConstructorAcceptsNaN_Test() + { + var r1 = new Rect(0, 0, double.NaN, double.NaN); + Assert.AreEqual(double.NaN, r1.Width); + } + + [TestMethod] + public void Rect_ConstructorAcceptsPositiveInfinity_Test() + { + var r1 = new Rect(0, 0, double.PositiveInfinity, double.PositiveInfinity); + Assert.AreEqual(double.PositiveInfinity, r1.Width); + } + + [TestMethod] + [ExpectedException(typeof(ArgumentException))] + public void Rect_ConstructorFailsNegativeInfinity_Test() + { + var r1 = new Rect(0, 0, double.NegativeInfinity, double.NegativeInfinity); + } + + [TestMethod] + public void Rect_AssignmentAcceptsNaN_Test() + { + var r1 = new Rect(); + + r1.Width = double.NaN; + Assert.AreEqual(double.NaN, r1.Width); + } + + [TestMethod] + public void Rect_AssignmentAcceptsPositiveInfinity_Test() + { + var r1 = new Rect(); + + r1.Width = double.PositiveInfinity; + Assert.AreEqual(double.PositiveInfinity, r1.Width); + } + + [TestMethod] + [ExpectedException(typeof(ArgumentException))] + public void Rect_AssignmentFailsNegativeInfinity_Test() + { + var r1 = new Rect(); + + r1.Width = double.NegativeInfinity; + } + + [TestMethod] + public void Size_ConstructorAcceptsNaN_Test() + { + var r1 = new Size(double.NaN, double.NaN); + Assert.AreEqual(double.NaN, r1.Width); + } + + [TestMethod] + public void Size_ConstructorAcceptsPositiveInfinity_Test() + { + var r1 = new Size(double.PositiveInfinity, double.PositiveInfinity); + Assert.AreEqual(double.PositiveInfinity, r1.Width); + } + + [TestMethod] + [ExpectedException(typeof(ArgumentException))] + public void Size_ConstructorFailsNegativeInfinity_Test() + { + var r1 = new Size(double.NegativeInfinity, double.NegativeInfinity); + } + + [TestMethod] + public void Size_AssignmentAcceptsNaN_Test() + { + var r1 = new Size(); + + r1.Width = double.NaN; + Assert.AreEqual(double.NaN, r1.Width); + } + + [TestMethod] + public void Size_AssignmentAcceptsPositiveInfinity_Test() + { + var r1 = new Size(); + + r1.Width = double.PositiveInfinity; + Assert.AreEqual(double.PositiveInfinity, r1.Width); + } + + [TestMethod] + [ExpectedException(typeof(ArgumentException))] + public void Size_AssignmentFailsNegativeInfinity_Test() + { + var r1 = new Size(); + + r1.Width = double.NegativeInfinity; + } + } +} diff --git a/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresVerificationTests.csproj b/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresVerificationTests.csproj new file mode 100644 index 00000000..d6b17885 --- /dev/null +++ b/Microsoft.Research/Contracts/SystemRequiresVerificationTests/SystemRequiresVerificationTests.csproj @@ -0,0 +1,89 @@ + + + + Debug + AnyCPU + {34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC} + Library + Properties + SystemRequiresVerificationTests + SystemRequiresVerificationTests + v4.0 + 512 + {3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} + 10.0 + $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) + $(ProgramFiles)\Common Files\microsoft shared\VSTT\$(VisualStudioVersion)\UITestExtensionPackages + False + UnitTest + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + + 3.5 + + + + + + + + + + + + + + + + + + + + + + + + + + False + + + False + + + False + + + False + + + + + + + + \ No newline at end of file diff --git a/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.GroupDescription.cs b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.GroupDescription.cs new file mode 100644 index 00000000..bafd89cf --- /dev/null +++ b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.GroupDescription.cs @@ -0,0 +1,100 @@ +using System; +using System.Collections.ObjectModel; +using System.Diagnostics.Contracts; +using System.Globalization; + +namespace System.ComponentModel +{ +#if !SILVERLIGHT && !NETFRAMEWORK_3_5 // => types defined in System.Windows! + // Summary: + // Provides an abstract base class for types that describe how to divide the + // items in a collection into groups. + public abstract class GroupDescription : INotifyPropertyChanged + { + // Summary: + // Initializes a new instance of the System.ComponentModel.GroupDescription + // class. + // protected GroupDescription(); + + // Summary: + // Gets the collection of names that are used to initialize a group with a set + // of subgroups with the given names. + // + // Returns: + // The collection of names that are used to initialize a group with a set of + // subgroups with the given names. + public ObservableCollection GroupNames + { + get + { + Contract.Ensures(Contract.Result>() != null); + return null; + } + } + + // Summary: + // Occurs when a property value changes. + // protected virtual event PropertyChangedEventHandler PropertyChanged; + + // Summary: + // Returns the group name(s) for the given item. + // + // Parameters: + // item: + // The item to return group names for. + // + // level: + // The level of grouping. + // + // culture: + // The System.Globalization.CultureInfo to supply to the converter. + // + // Returns: + // The group name(s) for the given item. + public abstract object GroupNameFromItem(object item, int level, CultureInfo culture); + // + // Summary: + // Returns a value that indicates whether the group name and the item name match + // such that the item belongs to the group. + // + // Parameters: + // groupName: + // The name of the group to check. + // + // itemName: + // The name of the item to check. + // + // Returns: + // true if the names match and the item belongs to the group; otherwise, false. + public virtual bool NamesMatch(object groupName, object itemName) + { + return false; + } + // + // Summary: + // Raises the System.ComponentModel.GroupDescription.PropertyChanged event. + // + // Parameters: + // e: + // Arguments of the event being raised. + //protected virtual void OnPropertyChanged(PropertyChangedEventArgs e); + + // + // Summary: + // Returns whether serialization processes should serialize the effective value + // of the System.ComponentModel.GroupDescription.GroupNames property on instances + // of this class. + // + // Returns: + // Returns true if the System.ComponentModel.GroupDescription.GroupNames property + // value should be serialized; otherwise, false. + // public bool ShouldSerializeGroupNames(); + + event PropertyChangedEventHandler INotifyPropertyChanged.PropertyChanged + { + add { throw new NotImplementedException(); } + remove { throw new NotImplementedException(); } + } + } +#endif +} diff --git a/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.ICollectionView.cs b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.ICollectionView.cs new file mode 100644 index 00000000..0dc1e9a5 --- /dev/null +++ b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.ICollectionView.cs @@ -0,0 +1,504 @@ +using System; +using System.Collections; +using System.Collections.ObjectModel; +using System.Collections.Specialized; +using System.Diagnostics.Contracts; +using System.Globalization; + +namespace System.ComponentModel +{ +#if !SILVERLIGHT && !NETFRAMEWORK_3_5 // => types defined in System.Windows! + + // Summary: + // Provides information for the System.ComponentModel.ICollectionView.CurrentChanging + // event. + public class CurrentChangingEventArgs : EventArgs + { + // Summary: + // Initializes a new instance of the System.ComponentModel.CurrentChangingEventArgs + // class. + public CurrentChangingEventArgs() { } + // + // Summary: + // Initializes a new instance of the System.ComponentModel.CurrentChangingEventArgs + // class with the specified isCancelable value. + // + // Parameters: + // isCancelable: + // A value that indicates whether the event is cancelable. + public CurrentChangingEventArgs(bool isCancelable) { } + + // Summary: + // Gets or sets a value that indicates whether to cancel the event. + // + // Returns: + // true if the event is to be canceled; otherwise, false. The default value + // is false. + // + // Exceptions: + // System.InvalidOperationException: + // If the value of System.ComponentModel.CurrentChangingEventArgs.IsCancelable + // is false. + public bool Cancel + { + get + { + return false; + } + set + { + + } + } + // + // Summary: + // Gets a value that indicates whether the event is cancelable. + // + // Returns: + // true if the event is cancelable, otherwise, false. The default value is true. + public bool IsCancelable + { + get + { + return false; + } + } + } + + // Summary: + // Represents the method that handles the System.Windows.Data.CollectionView.CurrentChanging + // event. + // + // Parameters: + // sender: + // The object that raised the event. + // + // e: + // Information about the event. + public delegate void CurrentChangingEventHandler(object sender, CurrentChangingEventArgs e); + + // Summary: + // Enables collections to have the functionalities of current record management, + // custom sorting, filtering, and grouping. + [ContractClass(typeof (ICollectionViewContract))] + public interface ICollectionView : IEnumerable, INotifyCollectionChanged + { + // Summary: + // Gets a value that indicates whether this view supports filtering via the + // System.ComponentModel.ICollectionView.Filter property. + // + // Returns: + // true if this view support filtering; otherwise, false. + bool CanFilter { get; } + // + // Summary: + // Gets a value that indicates whether this view supports grouping via the System.ComponentModel.ICollectionView.GroupDescriptions + // property. + // + // Returns: + // true if this view supports grouping; otherwise, false. + bool CanGroup { get; } + // + // Summary: + // Gets a value that indicates whether this view supports sorting via the System.ComponentModel.ICollectionView.SortDescriptions + // property. + // + // Returns: + // true if this view supports sorting; otherwise, false. + bool CanSort { get; } + // + // Summary: + // Gets or sets the cultural info for any operations of the view that may differ + // by culture, such as sorting. + // + // Returns: + // The culture to use during sorting. + CultureInfo Culture { get; set; } + // + // Summary: + // Gets the current item in the view. + // + // Returns: + // The current item of the view or null if there is no current item. + object CurrentItem { get; } + // + // Summary: + // Gets the ordinal position of the System.ComponentModel.ICollectionView.CurrentItem + // within the view. + // + // Returns: + // The ordinal position of the System.ComponentModel.ICollectionView.CurrentItem + // within the view. + int CurrentPosition { get; } + // + // Summary: + // Gets or sets a callback used to determine if an item is suitable for inclusion + // in the view. + // + // Returns: + // A method used to determine if an item is suitable for inclusion in the view. + Predicate Filter { get; set; } + // + // Summary: + // Gets a collection of System.ComponentModel.GroupDescription objects that + // describe how the items in the collection are grouped in the view. + // + // Returns: + // A collection of System.ComponentModel.GroupDescription objects that describe + // how the items in the collection are grouped in the view. + ObservableCollection GroupDescriptions { get; } + // + // Summary: + // Gets the top-level groups. + // + // Returns: + // A read-only collection of the top-level groups or null if there are no groups. + ReadOnlyObservableCollection Groups { get; } + // + // Summary: + // Gets a value that indicates whether the System.ComponentModel.ICollectionView.CurrentItem + // of the view is beyond the end of the collection. + // + // Returns: + // Returns true if the System.ComponentModel.ICollectionView.CurrentItem of + // the view is beyond the end of the collection; otherwise, false. + bool IsCurrentAfterLast { get; } + // + // Summary: + // Gets a value that indicates whether the System.ComponentModel.ICollectionView.CurrentItem + // of the view is beyond the beginning of the collection. + // + // Returns: + // Returns true if the System.ComponentModel.ICollectionView.CurrentItem of + // the view is beyond the beginning of the collection; otherwise, false. + bool IsCurrentBeforeFirst { get; } + // + // Summary: + // Returns a value that indicates whether the resulting view is empty. + // + // Returns: + // true if the resulting view is empty; otherwise, false. + bool IsEmpty { get; } + // + // Summary: + // Gets a collection of System.ComponentModel.SortDescription objects that describe + // how the items in the collection are sorted in the view. + // + // Returns: + // A collection of System.ComponentModel.SortDescription objects that describe + // how the items in the collection are sorted in the view. + SortDescriptionCollection SortDescriptions { get; } + // + // Summary: + // Returns the underlying collection. + // + // Returns: + // An System.Collections.IEnumerable object that is the underlying collection. + IEnumerable SourceCollection { get; } + + // Summary: + // When implementing this interface, raise this event after the current item + // has been changed. + event EventHandler CurrentChanged; + // + // Summary: + // When implementing this interface, raise this event before changing the current + // item. Event handler can cancel this event. + event CurrentChangingEventHandler CurrentChanging; + + // Summary: + // Returns a value that indicates whether a given item belongs to this collection + // view. + // + // Parameters: + // item: + // The object to check. + // + // Returns: + // true if the item belongs to this collection view; otherwise, false. + bool Contains(object item); + // + // Summary: + // Enters a defer cycle that you can use to merge changes to the view and delay + // automatic refresh. + // + // Returns: + // An System.IDisposable object that you can use to dispose of the calling object. + IDisposable DeferRefresh(); + // + // Summary: + // Sets the specified item to be the System.ComponentModel.ICollectionView.CurrentItem + // in the view. + // + // Parameters: + // item: + // The item to set as the System.ComponentModel.ICollectionView.CurrentItem. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // within the view; otherwise, false. + bool MoveCurrentTo(object item); + // + // Summary: + // Sets the first item in the view as the System.ComponentModel.ICollectionView.CurrentItem. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // an item within the view; otherwise, false. + bool MoveCurrentToFirst(); + // + // Summary: + // Sets the last item in the view as the System.ComponentModel.ICollectionView.CurrentItem. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // an item within the view; otherwise, false. + bool MoveCurrentToLast(); + // + // Summary: + // Sets the item after the System.ComponentModel.ICollectionView.CurrentItem + // in the view as the System.ComponentModel.ICollectionView.CurrentItem. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // an item within the view; otherwise, false. + bool MoveCurrentToNext(); + // + // Summary: + // Sets the item at the specified index to be the System.ComponentModel.ICollectionView.CurrentItem + // in the view. + // + // Parameters: + // position: + // The index to set the System.ComponentModel.ICollectionView.CurrentItem to. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // an item within the view; otherwise, false. + bool MoveCurrentToPosition(int position); + // + // Summary: + // Sets the item before the System.ComponentModel.ICollectionView.CurrentItem + // in the view as the System.ComponentModel.ICollectionView.CurrentItem. + // + // Returns: + // true if the resulting System.ComponentModel.ICollectionView.CurrentItem is + // an item within the view; otherwise, false. + bool MoveCurrentToPrevious(); + // + // Summary: + // Recreates the view. + void Refresh(); + } + + [ContractClassFor(typeof (ICollectionView))] + abstract class ICollectionViewContract : ICollectionView + { + event NotifyCollectionChangedEventHandler INotifyCollectionChanged.CollectionChanged + { + add + { + } + remove + { + } + } + + IEnumerator IEnumerable.GetEnumerator() + { + throw new NotImplementedException(); + } + + bool ICollectionView.CanFilter + { + get + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.CanGroup + { + get + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.CanSort + { + get + { + throw new NotImplementedException(); + } + } + + CultureInfo ICollectionView.Culture + { + get + { + throw new NotImplementedException(); + } + set + { + throw new NotImplementedException(); + } + } + + object ICollectionView.CurrentItem + { + get + { + throw new NotImplementedException(); + } + } + + int ICollectionView.CurrentPosition + { + get + { + throw new NotImplementedException(); + } + } + + Predicate ICollectionView.Filter + { + get + { + throw new NotImplementedException(); + } + set + { + throw new NotImplementedException(); + } + } + + ObservableCollection ICollectionView.GroupDescriptions + { + get + { + Contract.Ensures(Contract.Result>() != null); + throw new NotImplementedException(); + } + } + + ReadOnlyObservableCollection ICollectionView.Groups + { + get + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.IsCurrentAfterLast + { + get + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.IsCurrentBeforeFirst + { + get + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.IsEmpty + { + get + { + throw new NotImplementedException(); + } + } + + SortDescriptionCollection ICollectionView.SortDescriptions + { + get + { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + IEnumerable ICollectionView.SourceCollection + { + get + { + throw new NotImplementedException(); + } + } + + event EventHandler ICollectionView.CurrentChanged + { + add + { + throw new NotImplementedException(); + } + remove + { + throw new NotImplementedException(); + } + } + + event CurrentChangingEventHandler ICollectionView.CurrentChanging + { + add + { + throw new NotImplementedException(); + } + remove + { + throw new NotImplementedException(); + } + } + + bool ICollectionView.Contains(object item) + { + throw new NotImplementedException(); + } + + IDisposable ICollectionView.DeferRefresh() + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentTo(object item) + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentToFirst() + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentToLast() + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentToNext() + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentToPosition(int position) + { + throw new NotImplementedException(); + } + + bool ICollectionView.MoveCurrentToPrevious() + { + throw new NotImplementedException(); + } + + void ICollectionView.Refresh() + { + throw new NotImplementedException(); + } + } +#endif +} diff --git a/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.SortDescriptionCollection.cs b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.SortDescriptionCollection.cs new file mode 100644 index 00000000..25a5c250 --- /dev/null +++ b/Microsoft.Research/Contracts/WindowsBase/System.ComponentModel.SortDescriptionCollection.cs @@ -0,0 +1,177 @@ +using System; +using System.Collections.ObjectModel; +using System.Collections.Specialized; +using System.Diagnostics.Contracts; +using System.Runtime; + +namespace System.ComponentModel +{ +#if !SILVERLIGHT && !NETFRAMEWORK_3_5 // => types defined in System.Windows! + + // Summary: + // Defines the direction and the property name to be used as the criteria for + // sorting a collection. + public struct SortDescription + { + // + // Summary: + // Initializes a new instance of the System.ComponentModel.SortDescription structure. + // + // Parameters: + // propertyName: + // The name of the property to sort the list by. + // + // direction: + // The sort order. + // + // Exceptions: + // System.ArgumentNullException: + // The propertyName parameter cannot be null. + // + // System.ArgumentException: + // The propertyName parameter cannot be empty + // + // System.ComponentModel.InvalidEnumArgumentException: + // The direction parameter does not specify a valid value. + public SortDescription(string propertyName, ListSortDirection direction) + { + Contract.Requires(!String.IsNullOrEmpty(propertyName)); + } + + // Summary: + // Compares two System.ComponentModel.SortDescription objects for value inequality. + // + // Parameters: + // sd1: + // The first instance to compare. + // + // sd2: + // The second instance to compare. + // + // Returns: + // true if the values are not equal; otherwise, false. + //public static bool operator !=(SortDescription sd1, SortDescription sd2); + // + // Summary: + // Compares two System.ComponentModel.SortDescription objects for value equality. + // + // Parameters: + // sd1: + // The first instance to compare. + // + // sd2: + // The second instance to compare. + // + // Returns: + // true if the two objects are equal; otherwise, false. + //public static bool operator ==(SortDescription sd1, SortDescription sd2); + + // Summary: + // Gets or sets a value that indicates whether to sort in ascending or descending + // order. + // + // Returns: + // A System.ComponentModel.ListSortDirection value to indicate whether to sort + // in ascending or descending order. + //public ListSortDirection Direction { get; set; } + // + // Summary: + // Gets a value that indicates whether this object is in an immutable state. + // + // Returns: + // true if this object is in use; otherwise, false. + //public bool IsSealed { get; } + + // + // Summary: + // Gets or sets the property name being used as the sorting criteria. + // + // Returns: + // The default value is null. + //public string PropertyName { get; set; } + + // Summary: + // Compares the specified instance and the current instance of System.ComponentModel.SortDescription + // for value equality. + // + // Parameters: + // obj: + // The System.ComponentModel.SortDescription instance to compare. + // + // Returns: + // true if obj and this instance of System.ComponentModel.SortDescription have + // the same values. + //public override bool Equals(object obj); + // + // Summary: + // Returns the hash code for this instance of System.ComponentModel.SortDescription. + // + // Returns: + // The hash code for this instance of System.ComponentModel.SortDescription. + //public override int GetHashCode(); + } + + + // Summary: + // Represents a collection of System.ComponentModel.SortDescription objects. + public class SortDescriptionCollection : Collection, INotifyCollectionChanged + { + // Summary: + // Gets an empty and non-modifiable instance of System.ComponentModel.SortDescriptionCollection. + public static readonly SortDescriptionCollection Empty; + + // Summary: + // Initializes a new instance of the System.ComponentModel.SortDescriptionCollection + // class. + public SortDescriptionCollection() { } + + // Summary: + // Occurs when an item is added or removed. + // protected event NotifyCollectionChangedEventHandler CollectionChanged; + + event NotifyCollectionChangedEventHandler INotifyCollectionChanged.CollectionChanged + { + add + { + } + remove + { + } + } + + // Summary: + // Removes all items from the collection. + //protected override void ClearItems(); + // + // Summary: + // Inserts an item into the collection at the specified index. + // + // Parameters: + // index: + // The zero-based index where the item is inserted. + // + // item: + // The object to insert. + //protected override void InsertItem(int index, SortDescription item); + // + // Summary: + // Removes the item at the specified index in the collection. + // + // Parameters: + // index: + // The zero-based index of the element to remove. + //protected override void RemoveItem(int index); + // + // Summary: + // Replaces the element at the specified index. + // + // Parameters: + // index: + // The zero-based index of the element to replace. + // + // item: + // The new value for the element at the specified index. + //protected override void SetItem(int index, SortDescription item); + } +#endif +} diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyObject.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyObject.cs index f8b6cc7a..d342d51b 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyObject.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyObject.cs @@ -109,7 +109,7 @@ public void CoerceValue(DependencyProperty dp) public object GetValue(DependencyProperty dp) { Contract.Requires(dp != null); - Contract.Ensures(Contract.Result() != null); + // May return null if property type is not a value type! return null; } diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs index 5067be35..47bf34c4 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.DependencyProperty.cs @@ -70,14 +70,28 @@ private DependencyProperty() { } // Returns: // The type of the object that registered the property or added itself as owner // of the property. - extern public Type OwnerType { get; } + public Type OwnerType + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } // // Summary: // Gets the type that the dependency property uses for its value. // // Returns: // The System.Type of the property value. - extern public Type PropertyType { get; } + public Type PropertyType + { + get + { + Contract.Ensures(Contract.Result() != null); + return null; + } + } // // Summary: // Gets a value that indicates whether the dependency property identified by diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs index af2ee496..558cec0f 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs @@ -94,8 +94,8 @@ public struct Rect // : IFormattable // The height of the rectangle. public Rect(double x, double y, double width, double height) { - Contract.Requires(width >= 0.0); - Contract.Requires(height >= 0.0); + Contract.Requires((width >= 0.0) || double.IsNaN(width) || double.IsPositiveInfinity(width)); + Contract.Requires((height >= 0.0) || double.IsNaN(height) || double.IsPositiveInfinity(height)); Contract.Ensures(Contract.ValueAtReturn(out this).X == x); Contract.Ensures(Contract.ValueAtReturn(out this).Y == y); @@ -209,16 +209,16 @@ public double Height { get { - Contract.Ensures(this.IsEmpty || Contract.Result() >= 0.0 || Double.IsNaN(Contract.Result())); + Contract.Ensures(this.IsEmpty || Contract.Result() >= 0.0 || Double.IsNaN(Contract.Result()) || Double.IsPositiveInfinity(Contract.Result())); return default(double); } set { // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. - Contract.Requires(value >= 0.0 || Double.IsNaN(value)); + Contract.Requires((value >= 0.0) || Double.IsNaN(value) || Double.IsPositiveInfinity(value)); - Contract.Ensures(this.Height == value || Double.IsNaN(value)); + Contract.Ensures(this.Height == value); } } @@ -334,16 +334,16 @@ public double Width { get { - Contract.Ensures(this.IsEmpty || Contract.Result() >= 0.0 || Double.IsNaN(Contract.Result())); + Contract.Ensures(this.IsEmpty || Contract.Result() >= 0.0 || Double.IsNaN(Contract.Result()) || Double.IsPositiveInfinity(Contract.Result())); return default(double); } set { // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. - Contract.Requires(value >= 0.0 || Double.IsNaN(value)); + Contract.Requires(value >= 0.0 || Double.IsNaN(value) || Double.IsPositiveInfinity(value)); - Contract.Ensures(this.Width == value || Double.IsNaN(value)); + Contract.Ensures(this.Width == value); } } // @@ -364,7 +364,7 @@ public double X { // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. - Contract.Ensures(this.X == value || Double.IsNaN(value)); + Contract.Ensures(this.X == value); } } // @@ -385,7 +385,7 @@ public double Y { // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort. - Contract.Ensures(this.Y == value || Double.IsNaN(value)); + Contract.Ensures(this.Y == value); } } // Summary: diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs index 5598ccfb..007a3523 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs @@ -39,8 +39,8 @@ public struct Size // : IFormattable // The initial height of the instance of System.Windows.Size. public Size(double width, double height) { - Contract.Requires(width >= 0.0); - Contract.Requires(height >= 0.0); + Contract.Requires((width >= 0.0) || double.IsNaN(width) || double.IsPositiveInfinity(width)); + Contract.Requires((height >= 0.0) || double.IsNaN(height) || double.IsPositiveInfinity(height)); Contract.Ensures(Contract.ValueAtReturn(out this).Width == width); Contract.Ensures(Contract.ValueAtReturn(out this).Height == height); diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs index 3bfd731c..c2776d6b 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.Dispatcher.cs @@ -21,6 +21,17 @@ namespace System.Windows.Threading { + // Summary: + // Represents an operation that has been posted to the System.Windows.Threading.Dispatcher + // queue. + public sealed class DispatcherOperation + { + } + + public enum DispatcherPriority + { + } + public sealed class Dispatcher { private Dispatcher() { } @@ -41,11 +52,36 @@ private Dispatcher() { } //extern public event DispatcherUnhandledExceptionFilterEventHandler UnhandledExceptionFilter; - // public DispatcherOperation BeginInvoke(Delegate method, params object[] args); - //public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method); - // public DispatcherOperation BeginInvoke(Delegate method, DispatcherPriority priority, params object[] args); - // public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg); - // public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg, params object[] args); + public DispatcherOperation BeginInvoke(Delegate method, params object[] args) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + + public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + + public DispatcherOperation BeginInvoke(Delegate method, DispatcherPriority priority, params object[] args) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + + public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + + public DispatcherOperation BeginInvoke(DispatcherPriority priority, Delegate method, object arg, params object[] args) + { + Contract.Ensures(Contract.Result() != null); + return null; + } + // public void BeginInvokeShutdown(DispatcherPriority priority); //extern public bool CheckAccess(); @@ -55,7 +91,7 @@ private Dispatcher() { } public static Dispatcher FromThread(Thread thread) { - Contract.Ensures(Contract.Result() != null); + // May return null! return null; } diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.DispatcherObject.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.DispatcherObject.cs index e2df8317..6f755140 100644 --- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.DispatcherObject.cs +++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Threading.DispatcherObject.cs @@ -22,7 +22,15 @@ public abstract class DispatcherObject { protected DispatcherObject() { } - public Dispatcher Dispatcher { get { Contract.Ensures(Contract.Result() != null); return null; } } + public Dispatcher Dispatcher + { + get + { + // Note: a DispatcherObject that is not associated with a + // dispatcher is considered to be free-threaded and will return null. + return null; + } + } extern public bool CheckAccess(); diff --git a/Microsoft.Research/Contracts/WindowsBase/WindowsBase10.csproj b/Microsoft.Research/Contracts/WindowsBase/WindowsBase10.csproj index 0e4df119..a5974bca 100644 --- a/Microsoft.Research/Contracts/WindowsBase/WindowsBase10.csproj +++ b/Microsoft.Research/Contracts/WindowsBase/WindowsBase10.csproj @@ -189,6 +189,9 @@ false + + +