Contract.Ensures在多个对象/类链码未经证实的合同

Question

我有以下类的结构：

using System; 
using System.Collections.Generic; 
using System.Linq; 
using System.Text; 
using System.Diagnostics.Contracts; 

namespace contractsTest 
{ 
    class Program 
    { 
     static void Main(string[] args) 
     { 
      IService s = new Service(); 
      s.sendMessage(MessagesCreator.TestMessage); 
     } 
    } 

    class Service : IService 
    { 
     public void DoSomething(Message m) 
     { 
     } 
    } 

    static class MessageNames 
    { 
     public static string TestMessage 
     { 
      get 
      { 
       Contract.Ensures(!string.IsNullOrWhiteSpace(Contract.Result<string>())); 
       return "TestMessage"; 
      } 
     } 
    } 

    class Message 
    { 
     public Message(string _name) 
     { 
      Contract.Requires<ArgumentNullException>(!string.IsNullOrWhiteSpace(_name)); 
      Contract.Ensures(this.Name == _name); 
      this.Name = _name; 
     } 

     public string Name { get; private set; } 
    } 

    static class MessagesCreator 
    { 
     public static Message TestMessage 
     { 
      get 
      { 
       Contract.Ensures(Contract.Result<Message>() != null); 
       Contract.Ensures(Contract.Result<Message>().Name == MessageNames.TestMessage); 

       return new Message(MessageNames.TestMessage); 
      } 
     } 
    } 

    static class Extensions 
    { 
     public static void sendMessage(this IService service, Message m) 
     { 
      Contract.Requires<ArgumentNullException>(service != null); 
      Contract.Requires<ArgumentNullException>(m != null); 
      Contract.Requires<ArgumentNullException>(!string.IsNullOrWhiteSpace(m.Name)); 

      service.DoSomething(m); 
     } 
    } 

    [ContractClass(typeof(IServiceContract))] 
    interface IService 
    { 
     void DoSomething(Message m); 
    } 
    [ContractClassFor(typeof(IService))] 
    abstract class IServiceContract : IService 
    { 
     public void DoSomething(Message m) 
     { 
      Contract.Requires<ArgumentNullException>(m != null); 
      Contract.Requires<ArgumentException>(!string.IsNullOrWhiteSpace(m.Name)); 
      // Do Something   
     } 
    } 
} 

在主，我得到以下警告CodeContracts：要求未经证实！string.IsNullOrWhiteSpace（m.Name）

任何想法如何解决它？

如果我改变主要以：

static void Main(string[] args) 
{ 
    IService s = new Service(); 

    Message messagesCreatorTestMessage = MessagesCreator.TestMessage; 

    if (string.IsNullOrWhiteSpace(messagesCreatorTestMessage.Name)) 
     throw new InvalidOperationException(); 

    s.sendMessage(messagesCreatorTestMessage); 
} 

警告消失，但应该有这样做的其他更优雅的方式。

Answer 1

这是可能的，这就是问题所在：我怀疑你的意思是

// In the Message constructor 
Contract.Requires<ArgumentNullException>(!string.IsNullOrWhiteSpace(_componentName)); 

：

Contract.Requires<ArgumentNullException>(!string.IsNullOrWhiteSpace(_name)); 

这不是很清楚，我在那里_componentName甚至来自...

Answer 2

的Ensures在Message构造函数中只指定了当构造函数完成时条件为真;但并不表示该条件将在Message实例的生命周期中为真。

要做到这一点，使用Contract.Invariant方法：

class Message 
{ 
    [ContractInvariantMethod] 
    private void MessageInvariants() 
    { 
     Contract.Invariant(!string.IsNullOrWhiteSpace(Name)); 
    } 

    public Message(string _name) 
    { 
     Contract.Requires<ArgumentNullException>(!string.IsNullOrWhiteSpace(_name)); 
     Contract.Ensures(this.Name == _name); 
     this.Name = _name; 
    } 

    public string Name { get; private set; } 
}