using Microsoft.Contracts; public interface Collection { [Pure] int Size(); [Pure] bool LegalElement(object o); [Pure] bool Contains(object o); bool Add(object o); requires LegalElement(o); // Spec#'s default modifies clause allows a method to modify fields of the receiver and of objects owned by the receiver ensures Contains(o); ensures result ==> Size() == old(Size()+1); ensures !result ==> Size() == old(Size()); } public class CollectionTest { public void testAdd(Collection! coll, object e) modifies coll.*; { assume coll.Size() == 0 && coll.LegalElement(e); bool b = coll.Add(e); assert coll.Contains(e); assert b ==> coll.Size() == 1; } }