Kilitli Missing Contracts on Libraries

Kilitli

  • 10 Mart 2009 Salı 06:20
    Sahip
     
      Kod İçerir

    (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)

Tüm Yanıtlar

  • 13 Mayıs 2010 Perşembe 16:32
     
     
    decimal would be great! Thanks
  • 27 Mayıs 2010 Perşembe 16:21
     
     
    Dispatcher please!!!
  • 04 Haziran 2010 Cuma 16:15
     
     

    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

  • 04 Haziran 2010 Cuma 20:26
     
     

    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

  • 14 Haziran 2010 Pazartesi 01:20
     
     
    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.
  • 16 Haziran 2010 Çarşamba 19:41
     
     

    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


  • 06 Temmuz 2010 Salı 19:45
     
      Kod İçerir

    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
  • 06 Temmuz 2010 Salı 20:37
     
     

    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
    • Düzenleyen Dave Sexton 06 Temmuz 2010 Salı 20:41 Comment about read-only
    •  
  • 08 Temmuz 2010 Perşembe 20:06
    Sahip
     
     
    Looks like Enumerable.Select's are marked with Pure. What particular method do you have in mind?
    Cheers, -MaF (Manuel Fahndrich)
  • 12 Temmuz 2010 Pazartesi 01:30
     
     
    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

  • 16 Temmuz 2010 Cuma 00:22
     
     

    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.

     

  • 28 Temmuz 2010 Çarşamba 23:29
     
     

    We use Unity heavily, so IUnityContainer would be very helpful.

     

  • 13 Ağustos 2010 Cuma 15:24
     
     
    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
  • 21 Eylül 2010 Salı 20:38
     
      Kod İçerir
    I think that:
    SecurityBindingElement.CreateUserNameOverTransportBindingElement()
    Should Ensure not-null. Also there are the properties .LocalClientSettings and .LocalServiceSettings.
  • 18 Ekim 2010 Pazartesi 15:27
     
     

    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

  • 10 Kasım 2010 Çarşamba 20:54
     
     
    What about the XNA framework, or should I be asking those guys?
  • 22 Kasım 2010 Pazartesi 12:31
     
     
    X509Certificate2Collection.Find in the System.Security.Cryptography.X509Certificates namespace.
  • 02 Aralık 2010 Perşembe 02:47
     
     

    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.

  • 15 Aralık 2010 Çarşamba 10:11
     
     

    System.Windows.Forms.Control.DataBinding

    Property is never Nothing and could use an ensures

  • 27 Ocak 2011 Perşembe 15:45
     
     

    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

  • 31 Ocak 2011 Pazartesi 09:15
     
     

    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
  • 01 Şubat 2011 Salı 17:40
     
     

    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?

  • 02 Şubat 2011 Çarşamba 21:41
     
     

    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 ;)

  • 03 Şubat 2011 Perşembe 03:16
     
     

    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?

  • 18 Şubat 2011 Cuma 12:30
     
     

    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?

  • 24 Şubat 2011 Perşembe 23:13
    Sahip
     
     

    You can try using the "check assumptions" feature of the static checker.

    f

     

  • 24 Şubat 2011 Perşembe 23:19
    Sahip
     
     

    We will be happy to add those contracts. Can you help us by giving more details on which classes/methods?

     

    Thanks

    f

  • 25 Şubat 2011 Cuma 05:45
     
     

    System.Windows.Controls.Validation, PresentationFramework

    There are no contracts at all.

  • 01 Mart 2011 Salı 03:24
     
     

    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()')

  • 01 Mart 2011 Salı 09:22
     
     

    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

  • 03 Mart 2011 Perşembe 17:50
     
     
    Is there a way to express that for IDictionary<TKey, TValue> there is an implied condition that Count == Keys.Count == Values.Count ? 
    Burt Harris
  • 05 Mart 2011 Cumartesi 19:44
     
     

    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

  • 09 Mart 2011 Çarşamba 05:32
     
     
    TimeSpan.Zero.Milliseconds == 0

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

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

  • 09 Mart 2011 Çarşamba 06:16
     
     

    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

  • 09 Mart 2011 Çarşamba 22:55
     
      Kod İçerir

    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;
      }
    }

  • 10 Mart 2011 Perşembe 00:39
     
     

    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);


  • 10 Mart 2011 Perşembe 00:53
     
     

    PresentationFramework

    Contract.Ensures(Contract.Result != null)

    on 

    System.Windows.Controls.Grid.ColumnDefinitions

    and

    System.Windows.Controls.Grid.RowDefinitions


     

     

  • 10 Mart 2011 Perşembe 04:15
     
     

    PresentationFramework

    System.Windows.Data.Bindings cannot return null

     

  • 16 Mart 2011 Çarşamba 22:04
     
     
    System.Threading.Tasks.TaskExtensions.Unwrap and Unwrap<T> should require and ensure non-null.
  • 20 Mart 2011 Pazar 10:32
     
     

    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)

  • 20 Mart 2011 Pazar 11:47
     
     
    That should be result >= 0. The size can be 0 for structs with no actual members.
  • 20 Mart 2011 Pazar 13:21
     
     

    Alex, it cannot be 0. Just checked in debugger:

    struct X {}

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

  • 20 Mart 2011 Pazar 14:12
     
     

    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)

  • 21 Mart 2011 Pazartesi 19:17
     
     

    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

  • 23 Mart 2011 Çarşamba 19:28
     
     

    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)

     

  • 04 Mayıs 2011 Çarşamba 18:08
    Sahip
     
     

    TimeSpan.Zero is a readonly field to which we cannot attach a contract yet :-(

    f

  • 04 Mayıs 2011 Çarşamba 19:34
    Sahip
     
     

    i've added a contract. However please note that it returns != null if and only if the parameter is not null

     

    f

  • 09 Mayıs 2011 Pazartesi 14:32
     
     

    Please add to System.Windows.Application.LoadComponent(Uri resourceLocator):

    Requires(resourceLocator != null);

    Ensures(result != null);

  • 23 Mayıs 2011 Pazartesi 20:30
    Sahip
     
     

    Hi Alexey,

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

     

    thanks

    f

  • 24 Mayıs 2011 Salı 03:26
     
     

    System.Data.Sql.SqlDataSourceEnumerator.Instance

    cannot return null

    Neither can 

    System.Data.Sql.SqlDataSourceEnumerator.GetDataSources

  • 24 Mayıs 2011 Salı 07:15
     
     

    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.

  • 27 Mayıs 2011 Cuma 12:31
     
     

    Random.NextDouble() already has: Ensures result >= 0.0

    But it is missing: Ensures result < 1.0

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

     

  • 27 Mayıs 2011 Cuma 16:25
     
     
    IAsyncResult.AsyncWaitHandle != null
    Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com
  • 30 Mayıs 2011 Pazartesi 04:40
     
      Kod İçerir

    The FileStream constructor should have something like:

     

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

  • 30 Mayıs 2011 Pazartesi 04:45
     
      Kod İçerir

    Enum.HasFlag needs this for the static checker to be able to verify usages:

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

     

  • 06 Haziran 2011 Pazartesi 01:43
     
     
    BlockingCollection<T> in its entirety too please.
  • 08 Haziran 2011 Çarşamba 13:55
     
     
    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.
  • 21 Haziran 2011 Salı 16:59
     
     

    System.Windows.Controls.ListBox.SelectedItems

    Please add Ensures(result != null)

  • 22 Haziran 2011 Çarşamba 16:50
     
     

    System.Windows.Interop.WindowInteropHelper

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

  • 25 Haziran 2011 Cumartesi 21:07
     
     

    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

  • 26 Haziran 2011 Pazar 10:48
     
     

    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. 

  • 26 Haziran 2011 Pazar 18:30
     
     
    System.Environment.OSVersion needs an ensures(result != null) contract.
  • 27 Haziran 2011 Pazartesi 14:15
     
     
    System.IntPtr.Size needs some sort of contract. According to documentation, it can be 4 or 8 depending on platform bitness.
  • 29 Haziran 2011 Çarşamba 04:16
     
     
    System.Linq.Expressions.Expressions.AddAssign needs an Ensure(result != null) Contract.
  • 04 Temmuz 2011 Pazartesi 19:43
     
     

    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

     

  • 06 Temmuz 2011 Çarşamba 03:16
     
     
    No, it's perfectly valid for it to return null.
  • 14 Temmuz 2011 Perşembe 16:19
     
     

    XmlNode.set_InnerText should require value != null

    XmlNode.set_InnerXml should require value != null

    XmlNode.set_OuterXml should require value != null

     

  • 14 Temmuz 2011 Perşembe 20:59
     
     

    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.

  • 08 Ağustos 2011 Pazartesi 07:35
     
     

    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

  • 26 Ağustos 2011 Cuma 00:18
     
     
    AsyncOperationManager.CreateOperation(...) should ensures that the result is != null
  • 28 Ağustos 2011 Pazar 02:50
     
     

    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.


  • 31 Ağustos 2011 Çarşamba 10:20
     
     

    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
  • 04 Eylül 2011 Pazar 02:16
     
     

    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
    • Düzenleyen Dave Sexton 04 Eylül 2011 Pazar 02:17
    •  
  • 06 Eylül 2011 Salı 10:44
     
     
    HttpApplication.Server != null
  • 07 Eylül 2011 Çarşamba 10:36
     
     
    This doesn't work for ISet<T>.
  • 07 Eylül 2011 Çarşamba 10:37
     
      Kod İçerir

    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);
    
    


  • 16 Eylül 2011 Cuma 08:59
     
     
    1. System.Type.GetGenericTypeDefinition() != null
  • 17 Eylül 2011 Cumartesi 16:37
     
     
    System.Delegate.CreateDelegate() != null when throwOnBindFailure == true
  • 19 Eylül 2011 Pazartesi 13:04
     
     

    System.Linq.Enumerable.OfType<TResult>():

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

     

  • 20 Eylül 2011 Salı 21:15
     
     

    HttpWebRequest.GetRequestStream

    SqlConnection.CreateCommand

    SqlCommand.Parameters

    SqlCommand.ExecuteReader

    ConcurrentBag.ToArray

     

    can you have Pex generate all these for you?



    • Düzenleyen spongman 20 Eylül 2011 Salı 21:55
    • Düzenleyen spongman 20 Eylül 2011 Salı 22:31
    •  
  • 05 Ekim 2011 Çarşamba 20:34
     
     
    System.Data.DataRow.Table != null
  • 07 Ekim 2011 Cuma 23:19
     
     

    ParallelQuery<>.ToArray<>()

    And probably a bunch of other PLinq methods.

  • 13 Ekim 2011 Perşembe 09:05
     
     

     

    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))
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 09:09
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 10:39
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 10:49
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 10:56
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 10:59
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 11:36
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 11:37
    • Düzenleyen Dluk 13 Ekim 2011 Perşembe 12:10
    •  
  • 09 Kasım 2011 Çarşamba 02:24
     
     

    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
  • 21 Kasım 2011 Pazartesi 03:02
     
      Kod İçerir
    TaskScheduler.Current != null
    SaveFileDialog.InitialDirectory != null (get/set)
    DrawingVisual.RenderOpen() != null
    
  • 22 Kasım 2011 Salı 17:54
     
     

    System.Web.UI.WebControls.TextBox:

    Text != null

    Text.Length <= MaxLength

     

  • 22 Kasım 2011 Salı 17:59
     
     

    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.

  • 23 Kasım 2011 Çarşamba 05:03
     
     
    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.
  • 30 Kasım 2011 Çarşamba 02:45
     
     
    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


  • 01 Aralık 2011 Perşembe 20:30
     
     
    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 :)
  • 14 Aralık 2011 Çarşamba 23:09
     
     

    I *think* these are correct:

    Delegate.Method does not return null

    MethodInfo.GetMethodBody does not return null

    MethodBody.GetILAsByteArray does not return null

  • 22 Aralık 2011 Perşembe 10:35
     
     
    Assembly.LoadFrom(...) != null
  • 10 Ocak 2012 Salı 11:20
     
      Kod İçerir
    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
    • Düzenleyen Dluk 10 Ocak 2012 Salı 11:20
    • Düzenleyen Dluk 10 Ocak 2012 Salı 11:23
    • Düzenleyen Dluk 10 Ocak 2012 Salı 11:26
    •  
  • 11 Ocak 2012 Çarşamba 11:19
     
      Kod İçerir
    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)

  • 11 Ocak 2012 Çarşamba 12:14
     
     
    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
  • 12 Ocak 2012 Perşembe 22:19
     
     
    System.Linq.IQueryProvider, System.Core
    CreateQuery(Expression) Requires: (expression != null)
    Execute<TResult>(Expression) Requires: (expression != null)
    Execute(Expression) Requires: (expression != null)

    Brice Lambson
  • 18 Ocak 2012 Çarşamba 13:41
     
      Kod İçerir
    System.Xml.XmlNode.OwnerDocument != null System.Xml.XmlAttributeCollection.Append() != null
    • Düzenleyen Dluk 18 Ocak 2012 Çarşamba 14:15 added contract
    •  
  • 19 Ocak 2012 Perşembe 00:35
     
     
    RegistryKey.GetValue(string, object) != null if object != null
  • 26 Ocak 2012 Perşembe 15:57
     
     
    System.Web.Routing.RouteData.Values != null
  • 01 Şubat 2012 Çarşamba 09:26
     
      Kod İçerir
    System.Globalization.CultureInfo.CurrentUICulture.DateTimeFormat != null
  • 07 Şubat 2012 Salı 07:38
     
     
    The whole of ArraySegment
  • 08 Şubat 2012 Çarşamba 07:04
     
     

    System.ServiceModel.ServiceHostBase.ChannelDispatchers != null

    System.AppDomain.CurrentDomain.BaseDirectory.Length < 260

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

  • 14 Şubat 2012 Salı 02:21
     
     
    IPEndPoint, e.g. to Ensure() that Port is in the allowable range.
  • 17 Şubat 2012 Cuma 11:17
     
     
    System.Web.Script.Serialization.JavaScriptSerializer.Serialize(..) != null
  • 20 Mart 2012 Salı 14:55
     
     
    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);
  • 28 Mart 2012 Çarşamba 12:41
     
     

    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!)

  • 30 Mart 2012 Cuma 00:25
     
     

    *removed some invalid contracts*

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


    • Düzenleyen Porges 30 Mart 2012 Cuma 00:28
    • Düzenleyen Porges 30 Mart 2012 Cuma 00:59
    • Düzenleyen Porges 30 Mart 2012 Cuma 01:02
    •  
  • 30 Mart 2012 Cuma 00:37
     
     

    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.

  • 30 Mart 2012 Cuma 00:58
     
     

    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.

    • Düzenleyen Porges 30 Mart 2012 Cuma 01:01
    •  
  • 11 Nisan 2012 Çarşamba 22:13
     
     
    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

    • Düzenleyen James Albert 11 Nisan 2012 Çarşamba 22:14
    •  
  • 11 Nisan 2012 Çarşamba 22:27
     
     
    DateTime.Millisecond >= 0
    DateTime.Millisecond < 1000
  • 20 Nisan 2012 Cuma 16:41
     
     
    System.Diagnostics.Stopwatch.StartNew() != null
  • 20 Nisan 2012 Cuma 16:50
     
     
    System.Linq.Expressions.Expression<>.Compile() != null
  • 24 Nisan 2012 Salı 18:15
     
     
    System.Xml.XmlNode.OuterXml != null
  • 27 Nisan 2012 Cuma 07:45
     
     

    DateTime.get_Ticks() should ensure that the result is at most 3155378975999999999, not 3155378976000000000.

  • 16 Mayıs 2012 Çarşamba 09:47
     
     
    ICustomFormatter.Format should require format != null
  • 25 Temmuz 2012 Çarşamba 21:17
     
     

    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)

    • Düzenleyen James Albert 25 Temmuz 2012 Çarşamba 23:50
    • Düzenleyen James Albert 26 Temmuz 2012 Perşembe 00:02 Added more.
    • Düzenleyen James Albert 26 Temmuz 2012 Perşembe 00:05
    •  
  • 18 Ekim 2012 Perşembe 03:07
     
     
    System.Windows.Media.FormattedText:
    Width >= 0
    Height >= 0

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

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