[PPL-devel] Widening when CP0 is not included in CP1

[Roberto Bagnara]

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

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it