What can/should Pre/Post conditions do?


In the last post i dicussed the issue of interface invariants.  I'm currently enforcing interface invariants by writing them up in code and then running the concrete implementations of that interface against those tests.  However, that seems somewhat clunky.  I really would like to put these invariants on the interface and then have:



  1. The compiler check the invariants
  2. Have the runtime check the invariants (with the option to possibly disable if perf was affected).  This could be done in a similar way to aspect weaving.
  3. Have some unit testing system automatically extract those invariants into tests and then run every implementation against those tests

I would love to have some language wheri could do the following: 



    public interface ICollection<A>


    {


        /// <summary>


        /// Attempts to add an element into this collection


        /// </summary>


        /// <param name="element">The element to add into this collection</param>


        /// <returns>true if the element was successfully added, false otherwise</returns>


        bool Add(A element) {


            postcondition {


                if (result == true) {


                    this.Contains(element);


                }


            }


 


            postcondition {


                if (result == true) {


                    !this.Empty


                }


            }


        }


 


        /// <summary>


        /// Returns true if this collection is Empty, false otherwise.


        /// </summary>


        /// <value></value>


        bool Empty


        {


            get;


        }


 


        /// <summary>


        /// Removes all the elements contained in this collection.


        /// </summary>


        void Clear() {


            postcondition {


                this.Empty;


            }


        }


    }


However, it's interesting because this still wouldn't solve my earlier problem.  How would i write the invariant that after calling Clear that all references were released.  Is such a thing even testable? 


That raises another issue.  If something isn't even testable should it be an invariant?


Comments (14)

  1. damien morton says:

    Being able to annotate interfaces with pre and post conditions would be an amazing facility for C#. Maybe you can lean on the powers that be to put them in for C# 2.0 in the year or so they have before release. Its something that would add greatly to the utility of the interface concept; as it stands interfaces have no semantics save for comments.

    Speaking of releases, Im not clear on what you mean by ‘releasing references’ on collection items. Are you talking GC references or IDisposable references. If IDisposable, I imagine youd call something like this:

    TestCollection<IDisposable> c;

    c.ApplyToAll(delegate(x) { x.Dispose(); })

    c.Clear();

    where the signature of ApplyToAll is something like this:

    class TestCollection<T>

    {

    private delegate void Functor(T x);

    void ApplyToAll(Functor f)

    {

    foreach (T t in this) f(t);

    }

    }

    kinda ugly, however.

  2. Damien, what i mean is this:

    if i were to implement ArrayCollection.Clear in the following manner:

    void Clear() {

    count = 0;

    }

    instead of:

    void Clear() {

    array = new A[0];

    count = 0;

    }

    then while they would have the exact same semantics in terms of the collection, the ArrayCollection would still maintain internal references to the objects that had been previously added, and then would therefor not be GC’ed unless overwritten with subsequent adds.

  3. David Levine says:

    I’d opt for the form that released the references, otherwise you are liable to introduce some nasty memory leak problems into the system. The side-effects of an implementation should be minimized (and well-documented), and attention should be given to the cases where a consumer of a class is not well-behaved. IOW, consider the worst case as well as the normal case.

  4. damien morton says:

    I agree with David Levine. Clear should release all references. I cant think of a reson why I would want to prevent previously added items from being GC’ed, after calling Clear.

    Actually, I can think of a reson; a collection containing references to objects that were expensive to create; i.e. a caching collection. You wouldnt build this functionality into a basic collection, as it would introduce unnecessary coupling.

  5. damien morton says:

    The invariant after Clear() is Count==0 and/or IsEmpty==true.

  6. A agree with both of you. I don’t think the benefits of fast add after Clear are worth the potential memory leaks that could occur. Especially since those are extremely non-intuitive.

    Note: Damien, you mentioned the invariants in your last post. HOwever, both of those invariants are met just by setting count to 0. How do you specify the invariant that no references are held afterwards?

  7. damien morton says:

    The references problem corresponds to putting a constraint on what the internal state should be after an operation. Clearly, you cant specify internal state invariants in an interface, and you probably dont actually want to. You may end up implementing a caching collection that does keep references; its possible, but not part of the interface because its intended as transparent behaviour.

  8. Looks like something Attributes and Component Services are well suited for. Unit Testing engines could build tests based on the attributes, and if you run your class in a Context, you could intercept calls and provide pre and post conditions at run-time.

  9. nospamplease: Could you tell me a litte more about Component Services?

  10. D has this sort of syntax for <a href="http://www.digitalmars.com/d/dbc.html">design by contract</a>. I’m not really convinced it has any significant benefits over aspect weaving though.

  11. Hi Cyrus, I should have been more specific. There are two kinds of Component Services .NET provides, context-bound services and Enterprise Services. Enterprise services are available to classes derived from ServicedComponent which in turn inherits from ContextBoundObject.

    When an object lives in a Context, .NET can synchronize access to the group of objects within a context. It does this via a cross-context interception architecture. This allows the CLR (and your own code as well) to intercept calls to objects within a context.

    This article (http://msdn.microsoft.com/msdnmag/issues/02/03/AOP/) talks about building an Aspect Oriented Framework. Aspects would be a natural way to enforce pre-post processing.

  12. Erik, you’re probably right. It seems like pre/post conditions are a subset of the capabilities that aspects provide. However, I’m not sure how much work has been done with aspects to make them into compile time checks over runtime checks.

  13. Aspects are purely runtime. For compile time checks, you’ll definitely have to rewrite the compiler. Perhaps you can ask Eric Gunnerson and Anders nicely to add contracts to the C# language. 😉

  14. With some intelligent macros (like in http://www.nemerle.org/macros.html#attributes)

    you can easily embedd runtime checks into your methods:

    [Macros.PostScan]

    macro Requires (_ : TypeDecl, m : Method, assertion)

    {

    m.Body <- <[

    assert ($assertion, "The “Requires” contract has been violated.");

    $(m.Body)

    ]>

    }

    using them in this way

    [Requires (i != 4 && boo (i))]

    foo (i : int) : void { … }

    It is also possible to do some compile time checks (by analyzing code – macros are compiler plugins, which runs at compile-time) – although in general I doubt any resonable verification can be made, as problem of ensuring any general behaviour at compile time is undecidable.

    You can also take a look at:

    http://www.resolvecorp.com/Products.aspx

    which seems to be some substitute of general macro mechanism using System.Reflection

Skip to main content