locked
Stronger postconditions for interfaces that implement interfaces with weaker postconditions - how? RRS feed

  • Question

  • Let's say we're writing some library e.g. for drawing on the screen, and to allow our clients to communicate with our library, we're also writing an API, which contains, among other things, some interfaces describing what data should clients pass to our library methods, callback API etc. It seems that not only Code Contracts perfectly fit there, but that it might be the primary reason Code Contracts were designed at all.

    The interfaces, of course, do not contain any data, so there is no need to turn these into abstract classes. Additionally, the client will possibly want to derive their classes from some another classes (e.g. from their SuperDataEntity), so we even should avoid turning the interfaces into abstract classes.

    However, our data model is so enterprisey, that we cannot live without inheritance in interfaces. So, in the end, we get something like that in our base library:

    		[ContractClass(typeof(ContractShape))]
    		interface IShape
    		{
    			int numberOfVertices
    			{
    				get;
    			}
    		}
    
    		[ContractClassFor(typeof(IShape))]
    		abstract class ContractShape : IShape
    		{
    
    			#region IShape Members
    
    			public int numberOfVertices
    			{
    				get {
    					Contract.Ensures(Contract.Result<int>() > 0);
    					throw new NotImplementedException();
    				}
    			}
    
    			#endregion
    		}
    
    		[ContractClass(typeof(ContractTriangle))]
    		interface ITriangle : IShape {
    			
    			bool amIRight {
    				get;
    			}
    
    		}
    
    		[ContractClassFor(typeof(ITriangle))]
    		abstract class ContractTriangle : ITriangle {
    
    			#region ITriangle Members
    
    			public bool amIRight
    			{
    				get { throw new NotImplementedException(); }
    			}
    
    			#endregion
    
    			#region IShape Members
    
    			public int numberOfVertices
    			{
    				get {
    					Contract.Ensures(Contract.Result<int>() == 3);
    					throw new NotImplementedException();
    				}
    			}
    
    			#endregion
    		}
    
    


    The code above won't compile with the following error: warning CC1076: Contract class Test.Program+ContractTriangle cannot define contract for method Test.Program+IShape.get_numberOfVertices as its original definition is not in type Test.Program+ITriangle. Define the contract on type Test.Program+IShape instead.

    Of course, i cannot define the contract in question on IShape, because IShape may have any positive number of vertices, the additional restriction should be checked for Triangles only. In chapter 3 ("Contract inheritance") of the documentation defining the strongest postcondition is mentioned as the only type of contracts allowed in inherited classes (though it seems they may have thought of classes inheritance only); however, this is exact type of contracts which fails to compile in my example.

    Maybe i just don't understand something and i shouldn't want to do what i'm trying to do. Anyway, what should i do being in such an use case?

    Friday, August 26, 2011 4:07 PM

All replies

  • Hi,

    It does seem like it should be supported, but perhaps there's some technical limitation preventing it.

    Regardless, I don't see the problem with using an abstract class here since your interface does actually contain data, even though you've cleverly encoded it in the form of a post-condition.  :)  If you want to ensure that the value of a property is always consistent with the type of its interface, that's data.

    But perhaps this is just a makeshift example?  If you must stick with interfaces, then you can at least try strengthening the post-condition in a concrete implementation instead.  I believe the static checker will honor it.  There's really no difference whether you put the post-condition in the interface or your own concrete type; however, if your consumers are responsible for providing implementations, then I guess using an abstract class is your only choice.

    - Dave


    http://davesexton.com/blog

    Friday, August 26, 2011 4:53 PM
  • I don't see the problem with using an abstract class here since your interface does actually contain data, even though you've cleverly encoded it in the form of a post-condition.

    The numberOfVertices field is to be implemented by client in its interface implementation (it might be, let's say, SuperShape : SuperDataEntity, API.IShape { int API.IShape.numberOfVertices { get { return this.vertices.Length; } } }). It is "encoded" in postcondition of ITriangle only because, from one side, ITriangle is a specific interface of IShape base interface (there could be many things they share in common; also, some methods of our library may expect IShape, but should still work with ITriangle); and, from the other side, we wouldn't want for triangle to have less or more than three vertices (and code contracts seem to be perfect tool to telling the client about such a limitation).

     

     if your consumers are responsible for providing implementations

    Yes, they are.

    Friday, August 26, 2011 5:57 PM
  • Hi,

    I meant that ITriangle could be an abstract class, not IShape.  But it doesn't matter anyway if consumers are responsible for the implementation, then both have to be.

    - Dave


    http://davesexton.com/blog
    Friday, August 26, 2011 6:55 PM
  • Currently, the consumers probably already have CTriangles and CSquares. It would be much easier for consumers to implement API.ITriangle in their CTriangle, as opposed to inventing some proxy object, say, CTriangleForApi : API.CAbstractTriangle { private CTriangle consumerTriangle; override int numberOfVertices { get { return this.consumerTriangle.vertices.Length; } } }. You may object that consumer may use a lot of different APIs and should anyway create a proxy class for each api to make code maintainable, but in my project, there is no such problem (actually, it is more like a standartized data model + some tools to manipulate the read-only data in the model).
    Friday, August 26, 2011 8:13 PM
  • anyone?
    Thursday, September 1, 2011 10:14 AM
  • This is allowed for classes to extend in the same way, so I don't see any valid reason why it's disallowed on interfaces.

    Maybe it has something to do with making it possible to make unimplementable interfaces vs. having unsatisfiable method results via conflicting combinations of Ensures statements e.g. x >= 0 && x < 0.  Though it just seems like an oversight and not anything technical.

    Thursday, September 1, 2011 10:23 PM
  • Maybe it has something to do with making it possible to make unimplementable interfaces vs. having unsatisfiable method results via conflicting combinations of Ensures statements e.g. x >= 0 && x < 0.  Though it just seems like an oversight and not anything technical.

    The same objection applies to classes (currently, we can make unimplementable abstract class in the same fashion you suggest it to do with interfaces). The only differences between abstract classes and interfaces for developer are:

    1) Abstract classes can contain data and implementation bodies, while interfaces can not.

    2) Interfaces support multiple inheritance, while abstract classes do not (primarily due to 1)).

    Neither of the differences above justifies the restriction in question.

    Friday, September 2, 2011 10:37 AM
  • Nobody cares?
    Sunday, September 18, 2011 3:17 PM
  • Nobody cares?

    I care :)

    I just hit the same snag.  The following code generates the same error.

    [ContractClass(typeof(FooContract<>))]
    public interface IFoo<T> where T : class
    {
      T DoWork();
    }
    
    [ContractClassFor(typeof(IFoo<>))]
    internal abstract FooContract<T> : IFoo<T> where T : class
    {
      public T DoWork()
      {
        Contract.Ensures(Contract.Result<T> != null);
        throw new NotImplementedException();
      }
    }
    
    [ContractClass(typeof(FooBarContract))]
    public interface IBar : IFoo<string>
    {
    }
    
    [ContractClassFor(typeof(IBar))]
    internal abstract FooBarContract : IBar
    {
      public string DoWork()
      {
         Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<string>()), "stronger postcondition");
      }
    }
    


    Thursday, November 3, 2011 2:01 PM
  • Caring is different than having time...

    There is only one method here: IShape.numberOfVertices (or IFoo.DoWork in the other example). Interface inheritance is just the union of the interface members. So you are trying to indicate that if someone just implements IShape, they have one requirement: namely satisfying the postcondition of the method. But now you are trying to say that if they also implement ITriangle (IBar in the other examle), then their implementation must satisfy a stronger requirement. I understand the appeal of that, but it goes beyond the current design of Code Contracts. What if you write a class that implements IShape, but is a subclass of a class that implements ITriangle? Which contract should your implementation of IShape's method conform to?


    Mike Barnett
    Monday, November 21, 2011 7:29 PM
  • Hi, All.

    I can provide another example right from the BCL.

    As all you may know, BCL provides several interfaces for dealing with collections: ICollection<T>, IList<T> etc. Lets take a look at postconditions for the Add method from those interfaces:

    // From mscorlib.Contracts.dll
    [ContractClassFor(typeof(ICollection<>))]
    internal abstract class ICollectionContract<T> : ICollection<T>, IEnumerable<T>, IEnumerable
    {
        public void Add([MarshalAs(UnmanagedType.Error)] T item)
        {
            Contract.Ensures((bool)(this.Count >= Contract.OldValue<int>(this.Count)), null,
                                "this.Count >= Contract.OldValue(this.Count)");
        }
    }

    [ContractClassFor(typeof(IList<>))]
    internal abstract class IListContract<T> : IList<T>, ICollection<T>, IEnumerable<T>, IEnumerable
    {
        void ICollection<T>.Add([MarshalAs(UnmanagedType.Error)] T item)
        {
            Contract.Ensures((bool)(this.Count == (Contract.OldValue<int>(this.Count) + 1)),
                null"Count == Contract.OldValue(Count) + 1");
        }
    }

    Absolutely clear, that we have exactly the same situation in the BCL itself because IList<T> derives from ICollection<T> and postcondition for method Add is stronger (Count = OldCount + 1 is stronger than Count >= OldCound). This code compiles, builds and works ... unexpectedly for me, because if I create my custom class that implements IList<T> interface I don't have any option to fulfill IList<T>.Add postcondition because I don't know how to understand that this postcondition even exists.

    class CustomClass : IList<string>
    {
        private readonly List<string> _backingList = new List<string>();
        public void Add(string s)
        {
            // And what if I'll add s twice?
            _backingList.Add(s);
            _backingList.Add(s);
        }
    }

    Unfortunately neighter Static Checker nor code rewriter are aware about IList<T> postcondition. If you take a look into resulting CustomList.Add method (after rewriter) you'll noticed only postconditions from ICollection<T> but not from IList<T>. But if we'll change interfaces to base classes its all OK and resulting method will contains both postconditions.

    I'm curious why you provided stronger postcondition for IList<T> when nobody could use it? And I don't understand what's wrong if we'll add postconditions from all inherited interfaces.

    BTW, about Mike's quesion: "What if you write a class that implements IShape, but is a subclass of a class that implements ITriangle? Which contract should your implementation of IShape's method conform to?"

    I guess my implementation should conform to strongest postcondition and in this case to ITriangle. More over, we can face this situation in other form (and you're solving this already):

    [ContractClass(typeof(ShapeContract))]
    interface IShape
    {
        // Postcondition: Contract.Result<string>() != null
        string DoSomething();
    }

    [ContractClassFor(typeof(IShape))]
    abstract class ShapeContract : IShape
    {
        string IShape.DoSomething()
        {
            Contract.Ensures(Contract.Result<string>() != null);
            throw new NotImplementedException();
        }
    }

    [ContractClass(typeof(BaseShapeContract))]
    abstract class BaseShape : IShape
    {
        // Stronger postcondition: Contract.Result<string>() != string.Empty
        public abstract string DoSomething();
    }

    [ContractClassFor(typeof(BaseShape))]
    abstract class BaseShapeContract : BaseShape
    {
        public override string DoSomething()
        {
            Contract.Ensures(Contract.Result<string>() != string.Empty);
            throw new NotImplementedException();
        }
    }

    class CustomShape : BaseShapeIShape
    {
        public override string DoSomething()
        {
            // And what postcondition to use?
            // This method should conform to strongest postcondition!
            return string.Empty;
        }
    }

    [TestFixture]
    class TestCustomShape
    {
        [Test]
        public void TestDoSomething()
        {
            // Static checker didn't notice a problem, but rewriter added both
            // postconditions to method DoSomething, so this method fails with postcondition violation!
            var customShape = new CustomShape();
            var result = customShape.DoSomething();
            Assert.IsNotNullOrEmpty(result);

        }
    }

    Thanks,
    Sergey Teplyakov 
    Visual C# MVP

    Saturday, March 3, 2012 7:49 PM
  • Hi Mike,

    Sorry to bump a rather old discussion, but we are trying to deal with the same limitation.

    When a method or property has multiple Contract.Ensures statements, the contracts are interpreted as a conjuction. I.e. all post-conditions should hold after the method or property is evaluated. I don't see why the same approach couldn't be used in this case.

    What if you write a class that implements IShape, but is a subclass of a class that implements ITriangle? Which contract should your implementation of IShape's method conform to?

    Since the base class already implements ITriangle, it would be redundant to specify that the class implements IShape. Futhermore, because the post-condition on the specified method in IShape has a strict weaker post-condition than the one in ITriangle, it is automatically satisified.

    It would be more interesting if we have had two derived interfaces ISmallShape (number of vertices < 10) and IPolygon (number of vertices > 2) and now try to implement a class Triangle which implements both ISmallShape and IPolygon. To me it seems straightforward for the post-condition of Triangle.numberOfVertices to hold both post-conditions (the conjunction), effectively 2 < number of vertices < 10.

    [ContractClass(typeof(ISmallShapeContract))]
    public interface ISmallShape : IShape
    {
    }
    
    [ContractClassFor(typeof(ISmallShape ))]
    internal abstract class ISmallShapeContract : ISmallShape
    {
      public int numberOfVertices
      {
        get 
        {
          Contract.Ensures(Contract.Result<int>() < 10);
     
          throw new NotImplementedException();
        }
      }
    }
    
    [ContractClass(typeof(ISmallShapeContract))]
    public interface IPolygon : IShape
    {
    }
    
    [ContractClassFor(typeof(IPolygon))]
    internal abstract class IPolygonContract : IPolygon
    {
      public int numberOfVertices
      {
        get 
        {
          Contract.Ensures(Contract.Result<int>() > 2);
     
          throw new NotImplementedException();
        }
      }
    }
    

    Doesn't that seem a valid way of handling this to you? Or are there maybe other reasons why this doesn't fit the current design?

    Best regards,

    Ranco Marcus

    Wednesday, March 27, 2013 12:45 PM
  • Thanks for pointing out the problem in our contracts of IList<T>. Indeed, we tried to add a stronger post in IList for ICollection<T>.Add, but it doesn't work because there is no method specific to IList<T>.Add. From the .NET perspective, there is only a single method ICollection<T>.Add, and as Mike pointed out, we don't know when you mean a method to implement something else, since there is no entity that represents IList<T>.Add.

    The discussion here is good in that it points to a limitation that I would love to overcome, but it seems to be rooted in how .NET represents methods and method references and that there is no such thing as IList<T>.Add, or or ITriangle.numOfVertices.

    With abstract/classes that override/implement interfaces, the situation is different. Each override/implementation is its own new method and we can add contracts to those and resolve references to these more specialized methods.

    At the moment, I don't see how to overcome this problem.


    Cheers, -MaF (Manuel Fahndrich)

    Tuesday, April 2, 2013 3:45 PM
  • When you do interface inheritance, there are no new methods for the inherited ones. IShape.numberOfVertices is the only method that exists. There is no IPolygon.numberOfVertices method at all (look at the IL). That is why you cannot add contracts in interfaces to base interface methods.

    In abstract classes/implementations, it is different as the new methods actually exist and thus you can add contracts there.


    Cheers, -MaF (Manuel Fahndrich)

    Tuesday, April 2, 2013 3:47 PM