Postcondition Rules ( PostCondRule )

Definition

An instance P of type PostCondRule is a rule for the postcondition of a module M. It is represented by a collection of lists of tagged rules R₀,..., R_m. The list r_i, i $\geq$ 1 corresponds to the ith output parameter of M, i.e., m is the number of output parameters.

#include < AGD/PostCondRule.h >

Creation

PostCondRule

P(int m = 1)

creates an instance P of type PostCondRule initialized to a postcondition rule for m output parameters. Each list is initialized to the empty list.

Operations

int	P.num_param()	returns the number of parameters for which P is defined; more exactly it returns m.
leda_list<TaggedRule> &	P[int i]	returns the list Ri of rules corresponding to the ith parameter.
TaggedRule&	P.rule(int i, list_item it)
		returns the rule at list item it in Ri.
AgdKey	P.right(int i, list_item it)
		returns the right side of the rule at list item it in Ri.
const leda_list<TRLiteral>&	P.left(int i, list_item it)
		returns the left side of the rule at list item it in Ri.
void	P.del(int i, list_item it)
		deletes the item it in Ri.