Main Page | Modules | Namespace List | Class Hierarchy | Class List | Namespace Members | Class Members | Related Pages

Parma_Polyhedra_Library::BHRZ03_Certificate Class Reference

The convergence certificate for the BHRZ03 widening operator. More...

List of all members.

Public Member Functions

 BHRZ03_Certificate ()
 Default constructor.
 BHRZ03_Certificate (const Polyhedron &ph)
 Constructor: computes the certificate for ph.
 BHRZ03_Certificate (const BHRZ03_Certificate &y)
 Copy constructor.
 ~BHRZ03_Certificate ()
 Destructor.
int compare (const BHRZ03_Certificate &y) const
 The comparison function for certificates.
int compare (const Polyhedron &ph) const
 Compares *this with the certificate for polyhedron ph.


Detailed Description

The convergence certificate for the BHRZ03 widening operator.

Convergence certificates are used to instantiate the BHZ03 framework so as to define widening operators for the finite powerset domain.

Note:
Each convergence certificate has to be used together with a compatible widening operator. In particular, BHRZ03_Certificate can certify the convergence of both the BHRZ03 and the H79 widenings.


Member Function Documentation

int Parma_Polyhedra_Library::BHRZ03_Certificate::compare const BHRZ03_Certificate y  )  const
 

The comparison function for certificates.

Returns:
$-1$, $0$ or $1$ depending on whether *this is smaller than, equal to, or greater than y, respectively.
Compares *this with y, using a total ordering which is a refinement of the limited growth ordering relation for the BHRZ03 widening.


Generated on Fri Aug 20 20:04:45 2004 for PPL by doxygen 1.3.8-20040812