Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __                                  
			  / _`  _   /  /  o           
			 /   ) __) /  /  / /  / /\/| 
			(___/ (_/ (_ (_ / (__/ /   |  
                                                
			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 7 mars, 10h30

                                --------------
                                Mário Pereira
                                --------------

                                     LRI

                   =======================================
                   A Modular Way to Reason About Iteration
                   =======================================

Iteration is a central concept in programming. It can be as simple as a while
loop or a recursive function, but it can also appear as a more complex
artifact, such as a cursor, a higher-order iterator, a generator, or a lazy
list. When it comes to verifying the correctness of a program, we need tools
to reason about iteration. Typically, we provide a suitable loop invariant for
a while loop and a contract for a recursive function. We consider in this work
the problem of verifying programs where iteration is performed by other means,
such as cursors or higher-order iterators.

Our idea is to specify iteration in terms of the finite sequence of the
elements enumerated so far, and only those. In particular, we are able to deal
with non-deterministic and possibly infinite iteration. We also show how to
cope with the issue of an iteration no longer being consistent with mutable
data.

We validate our proposal using the deductive verification tool Why3 and the
cursors and higher-order iterators paradigms. For each paradigm, we verify
several implementations of iterators and client code. This is done in a
modular way, i.e., the client code only relies on the specification of the
iteration. Our contribution is twofold:

 1. An approach to specify an iteration process, independently of how it is
     implemented (cursor, higher-order function, etc.);

 2. A methodology to verify implementations and use of cursors and
     higher-order iteration functions.