[PPL-devel] Widening Operator

[Roberto Bagnara]

Enrico Oliosi wrote:
 > Dear Ppl group,
 > I finished my parser using the Ppl Lib and my last work has been
 > the while statement.
 > I read about widening operator in your user's manual (page 9) and
 > I read that there are some differences between your operator and
 > Halbwachs one.
 > I would like to know if you will implement this operator in next
 > version of the Ppl Lib or if there exists a way to approximate
 > the Halbwachs operator (now I introduce a token which terminates
 > the cicle after 10 iterations).

Dear Enrico,

I assume you are working with PPL 0.5, and that by "[our] operator"
you mean the BHRZ03 widening.  If so, notice that the widening proposed
in the PhD thesis of Nicholas Halbwachs (which is a refinement of the
one proposed by Patrick Cousot and Halbwachs himself in their POPL'78
paper) is already present in the version of the library you have,
where it is called H79.  So implementation of the Cousot & Halbwachs
widening and extrapolation operators are provided by methods

   void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0);
   void limited_H79_extrapolation_assign(const Polyhedron& y,
					const ConSys& cs,
					unsigned* tp = 0);
   void bounded_H79_extrapolation_assign(const Polyhedron& y,
					const ConSys& cs,
					unsigned* tp = 0);

whereas our improved versions (improved because on a single application
we get a result that is never worse) are made available by the methods

   void BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp = 0);
   void limited_BHRZ03_extrapolation_assign(const Polyhedron& y,
					   const ConSys& cs,
					   unsigned* tp = 0);

   void bounded_BHRZ03_extrapolation_assign(const Polyhedron& y,
					   const ConSys& cs,
					   unsigned* tp = 0);

Please, do not hesitate to come back to us if I have misunderstood
your question.

 > I want to thank all you for your help which was very important for me
 > and for my thesis.

Glad to be useful.

 > Your group will be cited in the thanks of my thesis.

Thanks!  When your thesis is finished, please do not forget to send
us an electronic copy.  As soon as we know more about the work you
have been doing, we would like to list it in our credits' page
at http://www.cs.unipr.it/ppl/Credits/
All the best,

    Roberto

P.S.  We will be releasing PPL 0.6 in a couple of days.  If you
       are not subscribed already, please subscribe to the
       (strictly moderated) PPL-announce mailing list to get the
       announcement.  This can be easily done at
       http://www.cs.unipr.it/mailman/listinfo/ppl-announce

-- 
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