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