locked
Missing Contracts on Libraries

    General discussion

  • (Update: please start a new thread for each request. This thread is too long.)

    If you are using the static contract checker, one of the main issues you are likely going to run into are missing postconditions on library methods you are calling.

    We are working on filling in gaps as fast as we can, but it is mainly driven by us or you finding where important gaps are. Ideally, we would go systematically through the libraries and annotate them. At the moment we don't have the man power.

    Please tell us where you find missing contracts and we'll get them in as quickly as we can.

    Also, here's a tip you can use to get you unstuck on a small number of missing contracts. I'm not advertising it as a general fix, just a work around to get that last few warnings out.

    Say you are making a call in your code arg0.M(arg1,..., argn) where M is missing contracts. Just use the refactoring to extract a method for arg0.M(arg1,..., argn), ideally a static method taking exactly these parameters.

    Then write the contracts on your extracted method and call the real method as follows:

     
    T Wrapper(T0 x0, ... Tn xn) {  
      Contract.Requires(...);  
      ...  
      Contract.Ensures( <missing post condition> );  
     
      var result = x0.M(x1,..,xn);  
     
      Contract.Assume( <missing post condition on result>);  
      return result;  


    The Contract.Assume simply tells the checker that the ensures is missing on M, but that we should now assume it. Of course, the factoring only makes sense if you are calling this method multiple times. Otherwise, you can just put the Assume after you call the original method.


    Cheers, -MaF (Manuel Fahndrich)

    Tuesday, March 10, 2009 6:20 AM

All replies

  • decimal would be great! Thanks
    Thursday, May 13, 2010 4:32 PM
  • Dispatcher please!!!
    Thursday, May 27, 2010 4:21 PM
  • I'd like to have contracts for the Linq extensions (e.g. Reverse). Is there a way to view the existing Contracts for the libraries?

    - Raphael

    Friday, June 04, 2010 4:15 PM
  • Hi Raphael,

    You can use reflector to open the *.contract.dll that ship with Code Contract to see which Contracts are available (which is actually a good way to study some real-world contracts examples)

    Victor

    Friday, June 04, 2010 8:26 PM
  • Enumerable.Select should be marked [Pure].  I guess MS decided otherwise because the selector delegate can have side effects, but Enumerable.Sum is marked [Pure] and has the same issue.
    Monday, June 14, 2010 1:20 AM
  • Here are my pain points.

     

    CompositionContainer (specifically GetExportedValue never returns null)

    ServiceBase (EventLog never returns null) [Done]

    ServiceEndpoint

    ServiceDescription

    ServiceEndpointsCollection

    ClientBase<> (Channel never returns null)

    EndpointAddess

    Assembly (specifically LoadFrom)

    X509Certificate

    ClientRuntime

    SyncronizedCollection<>

    DispatchRuntime

    EndpointDispatcher

     

    Thanks,

    Mike


    Wednesday, June 16, 2010 7:41 PM
  • Hi MaF,

    Please add the following contracts.

    System.Diagnostics:

    TraceSource.Switch
        Contract.Ensures(Contract.Result<SourceSwitch>() != null>

    ASP.NET:

    IBindableTemplate.ExtractValues
        Contract.Requires(container != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IOrderedDictionary>().Cast<DictionaryEntry>(), e => e.Key != null))

    Control.EnsureChildControls
        Contract.Ensures(ChildControlsCreated)

    Ensuring ChildControlsCreated makes it possible to define invariants such as the following in pages and user controls so that all of the designer-generated fields are considered non-null by the static checker.  Please let me know if there's a better solution.

    [ContractInvariantMethod]
    void ObjectInvariant()
    {
     Contract.Invariant(!ChildControlsCreated || label != null);
    }
    
    void DoSomething()
    {
     EnsureChildControls();
    
     Contract.Assert(label != null);
    }

    - Dave


    http://davesexton.com/blog
    Tuesday, July 06, 2010 7:45 PM
  • Hi,

    Please also add Contract.Ensures(!ChildControlsCreated) in the constructors for Control and all derived types.

    Edit: Or convince the ASP.NET team to add a breaking change and make this property read-only ;)

    - Dave


    http://davesexton.com/blog
    • Edited by Dave Sexton Tuesday, July 06, 2010 8:41 PM Comment about read-only
    Tuesday, July 06, 2010 8:37 PM
  • Looks like Enumerable.Select's are marked with Pure. What particular method do you have in mind?
    Cheers, -MaF (Manuel Fahndrich)
    Thursday, July 08, 2010 8:06 PM
  • Looks like Enumerable.Select's are marked with Pure. What particular method do you have in mind?

    Yes, Select is marked with Pure in the current version. I was running 1.4.30601.2.

    Thanks,
    Bruno

    Monday, July 12, 2010 1:30 AM
  • Could you please make an mscorlib.dll/System.Windows.Forms.dll/System.Xml.dll assemblies for 2.0 framework as well? (I assume they would just contain a subset of 4.0/3.5 types, so it won't be that much work)

    We're developing an application for which the 2.0 features are pretty much sufficient, so we support the clients with XP and .NET 2.0, but the absense of stdlib contracts makes code somewhat verbose.

     

    Friday, July 16, 2010 12:22 AM
  • We use Unity heavily, so IUnityContainer would be very helpful.

     

    Wednesday, July 28, 2010 11:29 PM
  • Count me in with mike's list of ServiceModel classes (and add ChannelFactory <>). Also, is it possible to specify our own contracts for the BCL? I have previously been able to create contracts for third party libraries; but although I have created a System.ServiceModel.Contracts.dll and am pointing my project to it, it doesn't seem to be having an effect. Is there a way to debug these kinds of issues?
    Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com
    Friday, August 13, 2010 3:24 PM
  • I think that:
    SecurityBindingElement.CreateUserNameOverTransportBindingElement()
    Should Ensure not-null. Also there are the properties .LocalClientSettings and .LocalServiceSettings.
    Tuesday, September 21, 2010 8:38 PM
  • Here are two:

    System.Data.SqlClient.SqlCommand.Parameters.Get
    add: Ensures(Result(Of SqlParameterCollection) IsNot Nothing)

    System.Data.SqlClient.SqlException.Get
    add: Ensures(Result (Of SqlErrorCollection) IsNot Nothing)

     

    And probably more properties under System.Data that will never return Nothing

    Monday, October 18, 2010 3:27 PM
  • What about the XNA framework, or should I be asking those guys?
    Wednesday, November 10, 2010 8:54 PM
  • X509Certificate2Collection.Find in the System.Security.Cryptography.X509Certificates namespace.
    Monday, November 22, 2010 12:31 PM
  • Hi,
    I creating a new type of Table control derived from TableLayoutPanel and I'm overriding some methods, namely OnCellPaint and OnControlAdded. These methods don't appear to have any contracts requiring that the event argument be != null.

    Toby.

    Thursday, December 02, 2010 2:47 AM
  • System.Windows.Forms.Control.DataBinding

    Property is never Nothing and could use an ensures

    Wednesday, December 15, 2010 10:11 AM
  • preconditions for

    System.Configuration.Provider.ProviderBase Initialize method

    and

    System.Configuration.SettingsProvider GetPropertyValues and SetPropertyValues methods

    and

    all methods on System.Web.Profile.ProfileBase, System.Web.Profile.ProfileProvider and System.Web.Security.MembershipProvider

    and

    the same for any other method for any other class derived from System.Configuration.Provider.ProviderBase I suppose.

    please

    Thursday, January 27, 2011 3:45 PM
  • Hi MaF,

    Please add PureAttribute to the System.Web.Mvc.AjaxRequestExtensions.IsAjaxRequest method so that it can be used in preconditions for ASP.NET MVC controller methods that are only intended to be called by AJAX requests.

    Thanks,
    Dave


    http://davesexton.com/blog
    Monday, January 31, 2011 9:15 AM
  • Are you asking about 2.0-3.5 framework types as well?  Or just 4.0?

    Is there any way to crowd-source the contracts?

    Tuesday, February 01, 2011 5:40 PM
  • There are various things missing in the LINQ extension methods. For example, Any should Ensure `Result == Contract.Exists(source, predicate)`. This might require a change to the signature of `Contract.Exists`, since that is a `Predicate<T>` and the LINQ methods take `Func<T,bool>` instead. I figure Code Contracts are more likely to change than System.Core ;)

    Wednesday, February 02, 2011 9:41 PM
  • A few of us here were thinking that can't code contracts automatically report back to you guys whenever we put in an Assume on a .NET CLR type?

    Yes there is a chance we will do an Assume wrongly - but this is something you can check?

    Thursday, February 03, 2011 3:16 AM
  • I've spotted a few missing contracts as well:

    • StackTrace and StackFrame
    • MEF classes (in System.ComponentModel.Composition)
    • System.Diagnostics.FileVersionInfo.GetVersionInfo (never returns null)
    • Reflection methods (e.g. Assembly.GetX methods)
    • System.Configuration.Install.InstallContext (Parameters property is never null)
    • TPL classes (in System.Threading.Tasks), e.g. Task.Factory is never null.

    What is the expected time frame from reporting missing contracts here to seeing them implemented in a future release of Code Contracts?

    Friday, February 18, 2011 12:30 PM
  • You can try using the "check assumptions" feature of the static checker.

    f

     

    Thursday, February 24, 2011 11:13 PM
  • We will be happy to add those contracts. Can you help us by giving more details on which classes/methods?

     

    Thanks

    f

    Thursday, February 24, 2011 11:19 PM
  • System.Windows.Controls.Validation, PresentationFramework

    There are no contracts at all.

    Friday, February 25, 2011 5:45 AM
  • Here are a couple more possible contracts to add:

    MemoryCache.Default (not null)

    Initializing log4net by using the class name throws a contract warning:

            private static readonly ILog _logger = LogManager.GetLogger(MethodBase.GetCurrentMethod().DeclaringType);

    (CodeContracts: Possibly calling a method on a null reference 'System.Reflection.MethodBase.GetCurrentMethod()')

    Tuesday, March 01, 2011 3:24 AM
  • It seems MethodBase.GetCurrentMethod() can actually return null.
    http://stackoverflow.com/questions/1799321/c-2-0-can-methodbase-getcurrentmethod-return-null
    But I also interested in under what conditionas it will return null.

    BTW, this method is very slow:
    http://stackoverflow.com/questions/4885582/methodbase-getcurrentmethod-performance

    Tuesday, March 01, 2011 9:22 AM
  • Is there a way to express that for IDictionary<TKey, TValue> there is an implied condition that Count == Keys.Count == Values.Count ? 
    Burt Harris
    Thursday, March 03, 2011 5:50 PM
  • 1. System.Environment.GetFolderPath(folder) has wrong Ensures(result.Length > 0). Actually result may be empty if folder doesn't exist

    2. Please add Ensures(result != null) to System.Environment.GetFolderPath(folder, option) overload

    Saturday, March 05, 2011 7:44 PM
  • TimeSpan.Zero.Milliseconds == 0

    static void DoStuff(TimeSpan x)
    {
    Contract.Requires(x.Milliseconds == 0);
    }

    static void Main(string[] args)
    {
    DoStuff(TimeSpan.Zero);

    Wednesday, March 09, 2011 5:32 AM
  • Now Rect has contracts the following have popped up:

     

    System.Windows.Controls.RowDefinition.ActualHeight

    System.Windows.Controls.ColumnDefinition.ActualWidth

    System.Windows.FrameworkElement.ActualHeight

    System.Windows.FrameworkElement.ActualWidth

    Wednesday, March 09, 2011 6:16 AM
  • System.Data.Objects.ObjectContext

     

    ObjectStateManager can not be null


    public ObjectStateManager ObjectStateManager
    {
      get
      {
        if (this._cache == null)
        {
          this._cache = new ObjectStateManager(this._workspace);
        }
        return this._cache;
      }
    }

    Wednesday, March 09, 2011 10:55 PM
  • Is there any way for a struct to prove behaviour after a call to the implicit constructor?

    ie: the assume should be able to be removed from the following code.

     

    var rect = new Rect();

    Contract.Assume(!rect.IsEmpty);


    Thursday, March 10, 2011 12:39 AM
  • PresentationFramework

    Contract.Ensures(Contract.Result != null)

    on 

    System.Windows.Controls.Grid.ColumnDefinitions

    and

    System.Windows.Controls.Grid.RowDefinitions


     

     

    Thursday, March 10, 2011 12:53 AM
  • PresentationFramework

    System.Windows.Data.Bindings cannot return null

     

    Thursday, March 10, 2011 4:15 AM
  • System.Threading.Tasks.TaskExtensions.Unwrap and Unwrap<T> should require and ensure non-null.
    Wednesday, March 16, 2011 10:04 PM
  • Please mark both overloads of System.Runtime.InteropServices.Marshal.SizeOf as [Pure] and add Ensures(result > 0) to them.

    And Marshal.SizeOf(Type t) should have Requires(t != null)

    And Marshal.SizeOf(object structure) should have Requires(structure != null)

    Sunday, March 20, 2011 10:32 AM
  • That should be result >= 0. The size can be 0 for structs with no actual members.
    Sunday, March 20, 2011 11:47 AM
  • Alex, it cannot be 0. Just checked in debugger:

    struct X {}

    Marshal.SizeOf(typeof(X)) == 1

    Sunday, March 20, 2011 1:21 PM
  • Please add the following Requires to System.Windows.Window properties:

    Left & Top: value >= int.MinValue && value <= int.MaxValue || double.IsNaN(value)

    Width & Height: value >= 0 && value <= int.MaxValue || double.IsNaN(value)

    Sunday, March 20, 2011 2:12 PM
  • The contracts for System.Windows.Rect are incomplete - all properties can be NaN.


    Requies for Width/Height setters should look like this:

     !this.IsEmpty
     value >= 0 || double.IsNaN(value)
     //OR: !(value < 0) -- shorter, but not sure if the static checker will properly handle this


    Ensures for Width/Height getters should be:

     this.IsEmpty || result >= 0 || double.IsNaN(value)
     //OR: this.IsEmpty || !(result < 0)


    Ensures for X/Y/Width/Height setters should be:

     this.X == value || double.IsNaN(value) && double.IsNaN(this.X)
     //OR: !(this.X != value)
     //OR: this.X.Equals(value)

    Contracts for System.Windows.Size have similar problem

    Monday, March 21, 2011 7:17 PM
  • More missing contracts for System.Windows.Rect:

    1. no contracts at all for Left/Top properties -- these are readonly accessors to X and Y and should ensure that Left == X and Top == Y

    2. X property ensures that when a Rect is empty then X is +Infinity; Width property should ensure that when a Rect is empty then Width is -Infinity (same for Height)

     

    Wednesday, March 23, 2011 7:28 PM
  • TimeSpan.Zero is a readonly field to which we cannot attach a contract yet :-(

    f

    Wednesday, May 04, 2011 6:08 PM
  • i've added a contract. However please note that it returns != null if and only if the parameter is not null

     

    f

    Wednesday, May 04, 2011 7:34 PM
  • Please add to System.Windows.Application.LoadComponent(Uri resourceLocator):

    Requires(resourceLocator != null);

    Ensures(result != null);

    Monday, May 09, 2011 2:32 PM
  • Hi Alexey,

      I've added it (i've deleted the previous post to mark this fact)

     

    thanks

    f

    Monday, May 23, 2011 8:30 PM
  • System.Data.Sql.SqlDataSourceEnumerator.Instance

    cannot return null

    Neither can 

    System.Data.Sql.SqlDataSourceEnumerator.GetDataSources

    Tuesday, May 24, 2011 3:26 AM
  • Hi Francecso,

    I thought it was some forum failure (the post disappeared so quickly). Since you added the contract for List<T>.Capacity, I delete the post.

    Thank you.

    Tuesday, May 24, 2011 7:15 AM
  • Random.NextDouble() already has: Ensures result >= 0.0

    But it is missing: Ensures result < 1.0

    NOTE: It's < 1.0, not <= 1.0

     

    Friday, May 27, 2011 12:31 PM
  • IAsyncResult.AsyncWaitHandle != null
    Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com
    Friday, May 27, 2011 4:25 PM
  • The FileStream constructor should have something like:

     

    Contract.Ensures(CanRead == access.HasFlag(FileAccess.Read));
    Contract.Ensures(CanWrite == access.HasFlag(FileAccess.Write));
    

    Monday, May 30, 2011 4:40 AM
  • Enum.HasFlag needs this for the static checker to be able to verify usages:

    Contract.Ensures(Contract.Result<bool>() == ((this & flag) == flag));
    

     

    Monday, May 30, 2011 4:45 AM
  • BlockingCollection<T> in its entirety too please.
    Monday, June 06, 2011 1:43 AM
  • TaskCompletionSource and Task are missing contracts. Biggest offenders are the TaskCompletionSource.Task member not being marked non-null, and Task.ContinueWith not ensuring non-null results.
    Wednesday, June 08, 2011 1:55 PM
  • System.Windows.Controls.ListBox.SelectedItems

    Please add Ensures(result != null)

    Tuesday, June 21, 2011 4:59 PM
  • System.Windows.Interop.WindowInteropHelper

    constructor public WindowInteropHelper(Window window)
    should have Contract.Requires(window != null) 

    Wednesday, June 22, 2011 4:50 PM
  • Shouldn't Collection<T>.Add()'s contract be: ensures this.Count = old(this.Count) + 1? Rather than ensures this.Count >= old(this.Count).

    Regards,
    Alex

    Saturday, June 25, 2011 9:07 PM
  • this.Count = old(this.Count) + 1 would be more restrictive then this.Count >= old(this.Count). 

    The current contract allows to create collections in which more then 1 item is added or even nothing when the Add method is called. There could be use cases for derived collection classes that duplicate items are ignored or use cases that more items are automatically added for some domain specific design rule. 

    Sunday, June 26, 2011 10:48 AM
  • System.Environment.OSVersion needs an ensures(result != null) contract.
    Sunday, June 26, 2011 6:30 PM
  • System.IntPtr.Size needs some sort of contract. According to documentation, it can be 4 or 8 depending on platform bitness.
    Monday, June 27, 2011 2:15 PM
  • System.Linq.Expressions.Expressions.AddAssign needs an Ensure(result != null) Contract.
    Wednesday, June 29, 2011 4:16 AM
  • Please add the following postconditions to the following System.Text.StringBuilder constructors:

        ensures result.Length == (value == null ? 0 : value.Length) to StringBuilder(string value);

        ensures result.Length == (value == null ? 0 : value.Length) to StringBuilder(string value, int capacity)

        ensures result.Length == length to StringBuilder(string value, int startIndex, int length, int capacity)

    The last one needs the following preconditions as well:

        requires startIndex >= 0

        requires length <= (value == null ? 0 : value.Length) - startIndex

     

    Monday, July 04, 2011 7:43 PM
  • No, it's perfectly valid for it to return null.
    Wednesday, July 06, 2011 3:16 AM
  • XmlNode.set_InnerText should require value != null

    XmlNode.set_InnerXml should require value != null

    XmlNode.set_OuterXml should require value != null

     

    Thursday, July 14, 2011 4:19 PM
  • If you violate this one, it's AccessViolationExceptions and ExecutionEngineExceptions all over town. :)

    Any character in a string cannot be NUL ('\0') or a large number of methods in the framework fail or do bad things to the stack.

    Thursday, July 14, 2011 8:59 PM
  • System.Web.HttpResponseBase.Cookies != null

    System.Web.HttpRequestBase.Cookies != null

    System.Net.WebRequest.Create(...) != null

     

    Some MVC stuff (seems like MVC team has no contract assemblies at all):

    System.Web.Mvc.GlobalFilters.Filters != null

    System.Web.Mvc.ControllerBase.ViewData != null

    Monday, August 08, 2011 7:35 AM
  • AsyncOperationManager.CreateOperation(...) should ensures that the result is != null
    Friday, August 26, 2011 12:18 AM
  • Sorry if this is the wrong thread, but I've noticed a small bug in an existing contract.

    In mscorlib.Contracts.dll:

    The System.Collections.DictionaryEntry contracts require the value of the Key property to be non-null (in the setter as well as the constructor).  The documentation (http://msdn.microsoft.com/en-us/library/system.collections.dictionaryentry.dictionaryentry.aspx) specifies that the non-null requirement was lifted with .NET 2.0.


    Sunday, August 28, 2011 2:50 AM
  • 1. Contract.Ensures(Contract.Result<ICryptoTransform>() != null) for set of methods SymmetricAlgorithm.CreateDecryptor / SymmetricAlgorithm.CreateEncryptor

    2. VirtualPathData.VirtualPath != null

    3. RouteTable.Routes != null

    4. ResourceSet.GetEnumerator() != null
    Wednesday, August 31, 2011 10:20 AM
  • Hi MaF,

    Please add non-null return value postconditions for all properties on these classes, if possible:

    • System.Windows.Input.ApplicationCommands
    • System.Windows.Input.ComponentCommands
    • System.Windows.Input.MediaCommands
    • System.Windows.Input.NavigationCommands
    • System.Windows.Documents.EditingCommands

    Thanks,
    Dave


    http://davesexton.com/blog
    • Edited by Dave Sexton Sunday, September 04, 2011 2:17 AM
    Sunday, September 04, 2011 2:16 AM
  • HttpApplication.Server != null
    Tuesday, September 06, 2011 10:44 AM
  • This doesn't work for ISet<T>.
    Wednesday, September 07, 2011 10:36 AM
  • Several contracts for char.ConvertFromUtf32:

     

    Contract.Ensures(Contract.Result<string>() != null);
    Contract.Ensures(Contract.Result<string>().Length >= 1);
    Contract.Ensures(Contract.Result<string>().Length <= 2);
    
    


    Wednesday, September 07, 2011 10:37 AM
  • 1. System.Type.GetGenericTypeDefinition() != null
    Friday, September 16, 2011 8:59 AM
  • System.Delegate.CreateDelegate() != null when throwOnBindFailure == true
    Saturday, September 17, 2011 4:37 PM
  • System.Linq.Enumerable.OfType<TResult>():

    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<TResult>>(), _ => _ != null));

     

    Monday, September 19, 2011 1:04 PM
  • HttpWebRequest.GetRequestStream

    SqlConnection.CreateCommand

    SqlCommand.Parameters

    SqlCommand.ExecuteReader

    ConcurrentBag.ToArray

     

    can you have Pex generate all these for you?



    • Edited by spongman Tuesday, September 20, 2011 10:31 PM
    Tuesday, September 20, 2011 9:15 PM
  • System.Data.DataRow.Table != null
    Wednesday, October 05, 2011 8:34 PM
  • ParallelQuery<>.ToArray<>()

    And probably a bunch of other PLinq methods.

    Friday, October 07, 2011 11:19 PM
  •  

    System.ServiceModel.Channels.Message.Headers != null

    System.ServiceModel.Channels.Message.CreateBufferedCopy() != null

    System.ServiceModel.Dispatcher.IClientMessageInspector contracts

    System.ServiceModel.Channels.MessageHeader contracts

    System.ServiceModel.Description.IEndpointBehavior contracts

    System.ServiceModel.Dispatcher.ClientRuntime.MessageInspectors != null


    System.Net.HttpWebResponse.GetResponseStream() != null (not sure)

    System.ServiceModel.OperationContext.Extensions != null

    System.ServiceModel.Dispatcher.ChannelDispatcher.Endpoints != null
    System.ServiceModel.Dispatcher.EndpointDispatcher.DispatchRuntime != null
    System.ServiceModel.Dispatcher.DispatchRuntime.MessageInspectors != null
     Guid.ToString()  : Ensures(!string.IsNullOrWhiteSpace(result))
    • Edited by Dluk Thursday, October 13, 2011 12:10 PM
    Thursday, October 13, 2011 9:05 AM
  • There really should be an easy way to add contracts to existing libraries.

    Instead of only executable contracts (DLLs) why not add the possibility to have just the metadata? Say an XML file with the contracts. This could be easily editable and upgradable.


    Paulo Morgado
    Wednesday, November 09, 2011 2:24 AM
  • TaskScheduler.Current != null
    SaveFileDialog.InitialDirectory != null (get/set)
    DrawingVisual.RenderOpen() != null
    
    Monday, November 21, 2011 3:02 AM
  • System.Web.UI.WebControls.TextBox:

    Text != null

    Text.Length <= MaxLength

     

    Tuesday, November 22, 2011 5:54 PM
  • there has to be a better way than this. how long has it been now since all these requests have been posted, and we haven't had an update?

    it's really a shame that you guys did all the hard work of writing the tool, but forgot the essential part of making it work effectively on anything more than the simplest test cases.

    Tuesday, November 22, 2011 5:59 PM
  • We don't expect acknowledgement to these. They are simply a request for contracts in a particular area. These DO get added, just not responded to in this forum.
    Wednesday, November 23, 2011 5:03 AM
  • System.Windows.Controls.ItemsControl:
    Items != null
    ItemContainerGenerator != null
    System.Windows.Controls.TextBox:
    Text != null (getter only - this may be set to null, but will just be coerced back to string.Empty)
    SelectionStart >= 0
    SelectionLen >= 0
    SelectionStart + SelectionLen <= Text.Length
    MaxLength >= 0
    System.Windows.UIElement:
     OnPreviewLostKeyboardfocus(KeyboardFocusChangedEventArgs e), e!= null
     OnPreviewKeyDown(KeyEventArgs e), e != null


    Wednesday, November 30, 2011 2:45 AM
  • This is what the contract reference DLLs are for, but there's no way to create one from scratch for another DLL at the moment... I guess you *could* craft one by hand :)
    Thursday, December 01, 2011 8:30 PM
  • I *think* these are correct:

    Delegate.Method does not return null

    MethodInfo.GetMethodBody does not return null

    MethodBody.GetILAsByteArray does not return null

    Wednesday, December 14, 2011 11:09 PM
  • Assembly.LoadFrom(...) != null
    Thursday, December 22, 2011 10:35 AM
  • sorry for no formatting, jquery script hangs in both FF and IE on that page for me ResourceSet.GetEnumerator() != null System.Web.HttpResponseBase.Cookies != null System.TimeZone.CurrentTimeZone != null System.Web.Routing.RouteTable.Routes != null System.Security.Cryptography.SymmetricAlgorithm.CreateEncryptor() != null System.Security.Cryptography.SymmetricAlgorithm.CreateDecryptor() != null System.Globalization.CultureInfo.Parent != null System.Net.WebRequest.Create(...) != null System.ServiceModel.Channels.MessageBuffer.CreateMessage() != null System.ServiceModel.Dispatcher.EndpointDispatcher.DispatchRuntime != null !string.IsNullOrWhiteSpace(Guid.ToString()) !string.IsNullOrEmpty(System.Reflection.AssemblName.Name) System.Web.HttpRequestBase.Params != null System.Web.HttpRequestBase.QueryString != null System.Globalization.CultureInfo.GetCultures() != null
    • Edited by Dluk Tuesday, January 10, 2012 11:26 AM
    Tuesday, January 10, 2012 11:20 AM
  • Some more:

    TypeDescriptor.GetConverter() != null
    
    DirectoryInfo.GetDirectories() != null
    DirectoryInfo.GetDirectories() Ensures: ForAll(Result, x => x != null)
    DirectoryInfo.GetFiles() Ensures: ForAll(Result, x => x != null)
    ICustomFormatter.Format() Requires: (format != null)

    Wednesday, January 11, 2012 11:19 AM
  • We can't expect that every consumer creates the contracts assembly. There must be a way to create contracts from the consumer side. Probably the team should focus on this first. -- Paulo Morgado http://www.PauloMorgado.NET/
    Paulo Morgado
    Wednesday, January 11, 2012 12:14 PM
  • System.Linq.IQueryProvider, System.Core
    CreateQuery(Expression) Requires: (expression != null)
    Execute<TResult>(Expression) Requires: (expression != null)
    Execute(Expression) Requires: (expression != null)

    Brice Lambson
    Thursday, January 12, 2012 10:19 PM
  • System.Xml.XmlNode.OwnerDocument != null System.Xml.XmlAttributeCollection.Append() != null
    • Edited by Dluk Wednesday, January 18, 2012 2:15 PM added contract
    Wednesday, January 18, 2012 1:41 PM
  • RegistryKey.GetValue(string, object) != null if object != null
    Thursday, January 19, 2012 12:35 AM
  • System.Web.Routing.RouteData.Values != null
    Thursday, January 26, 2012 3:57 PM
  • System.Globalization.CultureInfo.CurrentUICulture.DateTimeFormat != null
    Wednesday, February 01, 2012 9:26 AM
  • The whole of ArraySegment
    Tuesday, February 07, 2012 7:38 AM
  • System.ServiceModel.ServiceHostBase.ChannelDispatchers != null

    System.AppDomain.CurrentDomain.BaseDirectory.Length < 260

    System.Xml.XmlAttributeCollection.Append() != null

    Wednesday, February 08, 2012 7:04 AM
  • IPEndPoint, e.g. to Ensure() that Port is in the allowable range.
    Tuesday, February 14, 2012 2:21 AM
  • System.Web.Script.Serialization.JavaScriptSerializer.Serialize(..) != null
    Friday, February 17, 2012 11:17 AM
  • System.Linq.Enumerable.First()/Last() has: Contract.Requires(source.Count<TSource>() > 0, null, "Count(source) > 0"); propose: Contract.Requires(source.Any() || source.Count<TSource>() > 0, null);
    Tuesday, March 20, 2012 2:55 PM
  • Directory.Exists has this precondition:

    Contract.Requires((bool) (path != null), null, "path != null");

    This precondition is not needed, because Exists() returns false when path is null or empty (the same way File.Exists does, which has no precondition!)

    Wednesday, March 28, 2012 12:41 PM
  • *removed some invalid contracts*

    I think IDictionary should require key != null in several methods (this[], get, add, ...).


    • Edited by Porges Friday, March 30, 2012 1:02 AM
    Friday, March 30, 2012 12:25 AM
  • I believe MemberInfo.DeclaringType can be null for global methods (not supported in C# but can still happen) or DynamicMethods.

    Nullable.GetUnderlyingType() returns null if the passed in type is not a Nullable<> type.

    I seem to remember dictionaries support null keys as long as the equality comparer used also supports them.

    Friday, March 30, 2012 12:37 AM
  • Oops. I should have checked these beforehand... the reflection API seems to be at odds with the rest of the standard library, returning NULL when the argument is invalid.

    WRT dictionaries, the standard Dictionary class doesn't support null keys at all, even if the equality you've set does.

    • Edited by Porges Friday, March 30, 2012 1:01 AM
    Friday, March 30, 2012 12:58 AM
  • DateTimeOffset.Year > 0
    DateTimeOffset.Year <= 9999
    DateTimeOffset.Month > 0
    DateTimeOffset.Month <= 12
    DateTimeOffset.Day > 0
    DateTimeOffset.Day <= 31
    DateTimeOffset.Hour >= 0
    DateTimeOffset.Hour < 24
    DateTimeOffset.Minute >= 0
    DateTimeOffset.Minute < 60
    DateTimeOffset.Second >= 0
    DateTimeOffset.Second < 60
    DateTimeOffset.Millisecond >= 0
    DateTimeOffset.Millisecond < 1000

    Wednesday, April 11, 2012 10:13 PM
  • DateTime.Millisecond >= 0
    DateTime.Millisecond < 1000
    Wednesday, April 11, 2012 10:27 PM
  • System.Diagnostics.Stopwatch.StartNew() != null
    Friday, April 20, 2012 4:41 PM
  • System.Linq.Expressions.Expression<>.Compile() != null
    Friday, April 20, 2012 4:50 PM
  • System.Xml.XmlNode.OuterXml != null
    Tuesday, April 24, 2012 6:15 PM
  • DateTime.get_Ticks() should ensure that the result is at most 3155378975999999999, not 3155378976000000000.

    Friday, April 27, 2012 7:45 AM
  • ICustomFormatter.Format should require format != null
    Wednesday, May 16, 2012 9:47 AM
  • System.Globalization.RegionInfo.DisplayName != null

    System.ComponentModel.Composition.Hosting.AggregateCatalog.Catalogs != null

    System.Reflection.AssemblyName.Version != null

    System.Reflection.AssemblyName.Name != null

    or better yet...

    !string.IsNullOrWhiteSpace(System.Reflection.AssemblyName.Name)

    Wednesday, July 25, 2012 9:17 PM
  • System.Windows.Media.FormattedText:
    Width >= 0
    Height >= 0

    System.Windows.Thickness:
    Left >= 0
    Right >= 0
    Top >= 0
    Bottom >= 0

    System.Array:
    ConvertAll<,>(,) != null

    Thursday, October 18, 2012 3:07 AM