No formal specification is complete without pre- and post-conditions. A useful way to view these is as forming a contract between the object and its client. The pre-conditions define a state of the program which the client guarantees will be true before calling any method, whereas the post-conditions define the state of the program that the object's method will guarantee to create for you when it returns.
Again C (unlike Eiffel, for example) provides no formal support for pre- and post-conditions. However, the standard does define an assert function which can (and should!) be used to verify pre- and post-conditions [man page for assert]. We will see how this is used when we examine an implementation of our collection object. Thus pre- and post-conditions should be expressed as comments accompanying the method definition.
Adding pre- and post-conditions to the collection object would produce:
Select to load collection.h
Select to load collection.h
Aside
In order to keep the discussion simple at this stage, a very general specification of a collection has been implied by the definitions used here. Often, we would restrict our specification in various ways: for example, by not permitting duplicates (items with the same key) to be added to the collection. With such a collection, the pre- and post-conditions can be made more formal:
Select to load ucollection.h
Note how the pre- and post-conditions now use the FindInUCollection function to more precisely define the state of the object before and after the method has been invoked. Such formal pre- and post-conditions are obviously much more useful than the informal English ones previously specified. They are also easier to translate to appropriate assertions as will be seen when the implementation is constructed. Select to load ucollection.h
