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

• Anonymous
  May 16, 2004
  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.
  
  
  
  
• Anonymous
  May 16, 2004
  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.
  
  
• Anonymous
  May 16, 2004
  The comment has been removed
• Anonymous
  May 17, 2004
  The comment has been removed
• Anonymous
  May 17, 2004
  The invariant after Clear() is Count==0 and/or IsEmpty==true.
• Anonymous
  May 17, 2004
  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?
• Anonymous
  May 17, 2004
  The comment has been removed
• Anonymous
  May 17, 2004
  The comment has been removed
• Anonymous
  May 17, 2004
  The comment has been removed
• Anonymous
  May 17, 2004
  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.
• Anonymous
  May 18, 2004
  The comment has been removed
• Anonymous
  May 18, 2004
  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.
• Anonymous
  May 18, 2004
  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. ;)
• Anonymous
  May 24, 2004
  The comment has been removed