Next: Postcondition Rules ( PostCondRule Up: Pre- and Postconditions Previous: Preconditions ( PreCond ) Contents Index

Postconditions ( PostCond )

Baseclasses

$\begin{picture}(6.5,2.5) \thicklines \put(0,1.5){\framebox (5,1){\bf CondBase}... ...,2){\vector(0,-1){1}}\put(1.5,0){\framebox (5,1){\bf PostCond}} \end{picture}$

Definition

An instance P of type PostCond is a postcondition of a module M. It is represented by a collection of key sets S₀,..., S_m. The key set S_i, i $\geq$ 1 corresponds to the ith output parameter of M, i.e., m is the number of output parameters. The set S₀ has a special role. It represents the general postcondition of M.

#include < AGD/PostCond.h >

Creation

PostCond P(int m = 1) creates an instance P of type PostCond initialized to a postcondition for m output parameters. Each key set is initialized to the empty set.

Operations

PostCond inherits the operations of its base class CondBase.