locked
Why does the order of these contracts with OldValue matter? RRS feed

  • Question

  • Hi,

    Consider the following example.

    using System.Diagnostics.Contracts;
    
    namespace ContractLabs
    {
    	class Program
    	{
    		static void Main()
    		{
    		}
    
    		public static void Test(IFoo foo, int value)
    		{
    			Contract.Requires(foo != null);
    			Contract.Requires(foo.Enabled || value == foo.DisabledValue);
    
    			// foo.Do(value);		// No warnings
    
    			var clone = foo.Clone();
    
    			Contract.Assert(clone.Enabled == foo.Enabled);	// no warnings
    			Contract.Assert(clone.DisabledValue == foo.DisabledValue);	// no warnings
    
    			clone.Do(value);		// requires unproven: Enabled || value == DisabledValue
    		}
    	}
    
    	[ContractClass(typeof(IFooContract))]
    	public interface IFoo
    	{
    		bool Enabled { get; }
    		int DisabledValue { get; }
    
    		void Do(int value);
    		IFoo Clone();
    	}
    
    	[ContractClassFor(typeof(IFoo))]
    	internal abstract class IFooContract : IFoo
    	{
    		public bool Enabled
    		{
    			get
    			{
    				return false;
    			}
    		}
    
    		public int DisabledValue
    		{
    			get
    			{
    				return 0;
    			}
    		}
    
    		public void Do(int value)
    		{
    			Contract.Requires(Enabled || value == DisabledValue);
    		}
    
    		public IFoo Clone()
    		{
    			Contract.Ensures(Contract.Result<IFoo>() != null);
    			Contract.Ensures(Contract.Result<IFoo>().Enabled == Enabled);
    			Contract.Ensures(Contract.Result<IFoo>().DisabledValue == DisabledValue);
    			Contract.Ensures(Enabled == Contract.OldValue(Enabled));
    			Contract.Ensures(DisabledValue == Contract.OldValue(DisabledValue));
    			return null;
    		}
    	}
    }
    

    The requirement in Do is unproven on the clone; however, reversing the order in which the Clone method's post-conditions containing OldValue are stated prevents the warning.

    public IFoo Clone()
    {
    	Contract.Ensures(Contract.Result<IFoo>() != null);
    	Contract.Ensures(Enabled == Contract.OldValue(Enabled));
    	Contract.Ensures(DisabledValue == Contract.OldValue(DisabledValue));
    	Contract.Ensures(Contract.Result<IFoo>().Enabled == Enabled);
    	Contract.Ensures(Contract.Result<IFoo>().DisabledValue == DisabledValue);
    	return null;
    }
    

    This issue was hard to track down.

    Does the ordering of these contracts actually matter semantically?  It doesn't seem so to me.  Could the static checker be modified so that the order is irrelevant?

    Thanks,
    Dave


    http://davesexton.com/blog
    Monday, October 24, 2011 1:18 PM