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?