Next: Postconditions ( PostCond ) Up: Pre- and Postconditions Previous: Base Class for Pre- Contents Index

Preconditions ( PreCond )

Baseclasses

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

Definition

An instance P of type PreCond is a precondition of a module M. It is represented by a collection of key sets S₁,..., S_n. The key set S_i corresponds to the ith input parameter of M, i.e., n is the number of input parameters.

#include < AGD/PreCond.h >

Creation

PreCond P(int n = 1) creates an instance P of type PreCond initialized to a precondition for n input parameters. Each key set is initialized to the empty set.

Operations

PreCond inherits the operations of its base class CondBase.