Mario Mendez wrote:
Hi,
In the documentation you always remark the precondition CP0<=CP1 required by widening(CP1,CP0). What is the usual strategy when the condition is not met? I mean, imagine a list of consecutive abstract values (1D polyhedrons) like {1<x<2}, {2<x<3},{3<x<4}, ....,{n<x<n+1} How can we ensure converge in these cases?
Dear Mario,
widening is normally used to force or accelerate convergence of an iteration sequence that represents increasingly larger sets of program states. So, if at iteration k our analysis has determined that at program point p any set of states contained in S possible, at iteration k+1 and for the same program point the analysis will come up with a revised set of states S' that is larger than or equal to (i.e., that set-theoretically contains) S. When you use convex polyhedra, the condition between successive sets of states becomes inclusion between polyhedra.
The specific example you give,
{1<x<2}, {2<x<3},{3<x<4}, ....,{n<x<n+1}
does not seem to come from such an iteration sequence: a poly-hull operation seems to be missing so as to have the sequence
{1<x<2}, {1<x<3},{1<x<4}, ....,{1<x<n+1}
which satisfies the applicability condition of the widenings. All the best,
Roberto