In a previous post we have talked about components and interfaces. We believe that components are an essential and widely applicable extension to C is the basis for meaningful reuse and variability management. In our approach, the same interface can be provided (implemented) by several different components, in different ways. Of course, the semantics implied by the interface should be realized consistently by all these components. To enforce this, an interface must specify more than just the signature of the operations.
We have implemented two additional facilities: pre- and post conditions as well as protocol state machines.
Preconditions express constraints over the arguments of operations when they are called. The figure below shows an example. In the add operation, two preconditions are used to make sure the arguments are greater than zero. Postconditions ensure that the result is positive and the result is the sum of the two arguments. The Computer component below, which implements the interface, will verify the correctness of these constraints when operations are called. If they are violated, the message associated with the pre or postcondition is reported. Note that the pre and postconditions are expressed over the interface, and all components that provide the interface automatically get the verification code.
Sometimes postconditions have to be expressed over the state of an object. Since interfaces cannot define state, we have to use query operations to access the state. A query operation is an idempotent operation, that can be called at any time to return a value. In the example below, the value operation is marked as a query and hence can be used in pre and postconditions. Note also how the old keyword can be used to access the result of the value operation before the operation is executed.
The other ingredient to contractual interfaces are protocol state machines. These can be used to enforce the sequencing of calls on an interface. Take a look at the code below. It defines a protocol for each operation. The openForWrite operation requires the protocol state machine to be in the init state, and when called, transitions to the writing state. Once in writing, you can call write any number of times and then call close to go back to the init state. Reading works similarly. Essentially, the protocol state machine in the example enforces that the file system can be used for writing only or for reading only. Close resets it. The init state is the default state available in any protocol state machine. The * state is a shorthand for any state. Using the new keyword, new states can be introduced, and those can be referenced from other protocols. An operation can have several protocols, they are or’ed together.
Pre and Postconditions and protocols can be mixed. This way, a relatively complete specification of an interface’s semantics can be provided. The constraints are automatically checked on every implementing component, enforcing the contract.