De CeProMi.

Sommaire 1 programmes jouets challenge 1.1 memory manager 1.2 gen_sym, ou gen_prime 1.3 modules, invariants et partages 1.4 calculateur de Morgan 1.5 reference sur variable privée 1.6 tableaux persistants 1.7 effets et ordre supérieur 1.8 Crible 1.9 Wrapper liste+longueur 1.10 graphe cyclique 2 structures auto-réorganisantes 3 Raffinement de programmes Java

programmes jouets challenge

memory manager

• free list : est cachee

gen_sym, ou gen_prime

modules, invariants et partages

• author: Sylvain
• code: pseudo Ocaml
• probleme(s): invariant versus partage
• solution(s)?:
  • le choix de la politique d'invariant est crucial
  • une politique "simple" assume l'invariant a une pre et une post automatique, mais ceci va en l'encontre de la modularite: le client doit s'assurer que l'invariant est vrai
  • pour avoir de la modularite', il faut qu'un invariant soit attache a un scope : propriete de separation, ou de capacite

Sur l'exemple ci-dessous:

module A = struct
  let x = ref 0 { INVARIANT x >= 0 }
  let incr () = x:=!x+1 
end 

module B = struct
  let y = ref (2 * !A.x)  { INVARIANT y=2*A.x }
  let reset () = y:=2 * !A.x
  let foo () = y:=!y+2 ; A.incr() 
end 

module C = struct
  let y = ref (2 * !A.x + 1) { INVARIANT y=2*A.x+1 }
  let reset () = y:=(2 * !A.x + 1)
  let foo () = y:=!y+2 ; A.incr() ;
end 

On aimerait accepter certaines sequences d'appels qui n'invalident pas les invariants:

B.sync() ; B.foo() ; B.foo() ; C.sync() ; C.foo() ; C.foo() ;

Sur d'autres, on aimerait exprimer que toutes les sequences d'appels sont acceptables:

module Buff = struct
  let l = ref []
  let prem = ref 0 { INVARIANT 0 <= prem <= List.length l }
  let add x = l:= !l @ [x]
  let remove () = 
      if !prem < List.length !l then 
        let v=List.nth !l !prem in prem:=!prem+1 ; v
      else 0
end 

module Producer = struct
  let next = ref 1 
   { INVARIANT Buff.l = liste des ent. entre 1 et (next-1) }
  let step () = Buff.add !next ; next:=!next+1 
end 

module Consumer = struct
  let s = ref 0 
      { INVARIANT s = somme des elts de la sous-liste de 
          Buff.l entre indice 0 et indice (Buff.prem-1) }
  let step () = s:=!s + Buff.remove()
end 

calculateur de Morgan

• author: Morgan, revisité par Wendi
• code: pseudo-Java/JML
• probleme(s):
  • raffinement
  • effets privés cachés, effets publics sur variable modèle
• solution(s)?: appartenance, capacité

interface I {
	  
      //@ model bag<double> b;

      //@ assigns b;
      //@ ensures b == empty;
      void reset();

      //@ assigns b;
      //@ ensures b == union(\old(b),x);      
      void add(double x);

      //@ requires b != empty;
      //@ assigns \nothing
      //@ ensures \result == sum_bag(b) / cardinal(b);
      double mean();

}

class A implements I {
      
      private double sum = 0.0;
      private int count = 0;
      //@ invariant sum == sum_bag(b);
      //@ invariant count == cardinal(b);

      void reset() { sum = 0.0; count = 0; }

      void add(double x) { sum += x; count++; }

      double mean() { return sum/count; }

}

modification minime erronee:

     private static double sum = 0.0;
     private static int count = 0;

-> deux objets de classe A partagent ces variables -> on retombe sur l'exemple de Sylvain

reference sur variable privée

• author: Claude
• code: pseudo-Java/JML
• probleme(s): reference publique sur variable privée
• solution(s)?: appartenance, capacité

class A {
      private int t[1] = { 0 }; invariant t[0] % 2 == 0;
      
      //@ assigns \nothing;
      //@ ensures \result % 2 == 0;
      public int m() { t[0] += 2 ; return t[0]; }

      // flawed method: returns a reference to private data
      public int [] flaw() { return t; }
}

tableaux persistants

• author: François, Jean-Christophe
• code: pseudo Caml
• probleme(s):
  • effets de bords cachés, interface purement fonctionnelle
  • langage de spec approprié
  • qu'est -ce que le tas dans la logique ?
• solution(s)?:
  • une solution avec anti-frame (fpottier) (sans assertions logiques) (voir ci-dessous)

Faire un exposé sur un programme similaire en Java, Krakatoa -> Claude (ou Jessica ? -> Romain)

interface :

  logic type tab_logic
  
  logic create_logic : int -> int -> tab_logic
  (* [create_logic n x]: tableau de 0 a n-1, cases initialisee a x *)

  type tab

  logic repr : tab -> tab_logic -> prop

  val create : (n:int) { n >= 0 } -> (t:tab) { repr t (create_logic n 0) }

  val set : (t:tab) -> TODO

  val get : (t:tab) -> TODO

implantation:

   type data = Arr of int array 
    | Diff of int * int * tab  

   and tab = data ref   

   logic repr (t:tab) (tt:tab_logic) =
       repr_data !t tt

   and repr_data (d:data) (tt:tab_logic) =
       match d with
        | Arr a ->   
           forall i, 0 <= i < Array.length a ==>
              Array.get a i == logic_array_get tt i
        | Diff (i,v,t') ->
              (* conditions sur indice i ? *)
              forall tt', repr t' tt' ==>
                repr_data d (logic_array_update tt' i v)        

   let create n = ref (Arr (Array.create n 0)) 

  val set : (t:tab) -> TODO

  val get : (t:tab) -> TODO

Je (fpottier) vois les tableaux persistants comme un exemple typique de structure de données où la présence d'un état interne mutable peut être cachée via une règle de typage comme "anti-frame". Voici ce que cela pourrait donner dans un langage à la ML, doté du système de types que nous avons développé avec Arthur, et de la règle anti-frame. Note: dans un premier temps au moins, je ne traite que le typage, pas la spécification logique. Le résultat que j'obtiens par le typage est donc: il est bel et bien permis de cacher les modifications de l'état interne, cela ne compromet pas le raisonnement du client. (En gros, en termes JML: la clause "assigns nothing" est valide.) Pour ce qui est de vérifier que les tableaux persistants implémentent bien des tableaux, on peut le faire, mais ce sera pour une autre fois.

(* Assume given a primitive type constructor iarray for (tracked)
   imperative arrays, together with operations imkarray, iget,
   iset. *)

(* This is an interface for (persistent) arrays. An array is represented
   as a pair get/set functions. This view is equivalent to a Java-style
   interface. Note that this is a recursive type definition. *)

def type array alpha =
  (int -> alpha) * (int * alpha -> array alpha)

(* This is an internal type definition for persistent arrays, represented
   as a list of differences with respect to a base imperative array. The
   definition is parameterized over a singleton region sigma, which contains
   the base array, and a group region rho, which contains the cells. A cell
   is a reference to either the base array, or a diff, that is, a triple of
   of an index, a value, and a pointer to another cell. *)

(* Note: (cell alpha rho sigma) under R is equal to
   cell (alpha under R) rho sigma. *)

def type cell alpha rho sigma =
  ref (Base [sigma] + Diff (int * alpha * [rho]))

(* This is an internal capability definition. It is a separating
   conjunction of a singleton capability for the base array and a
   group capability for the cells. *)

(* Note: (invariant alpha rho sigma) under R is equal to
   invariant (alpha under R) rho sigma. *)

def type invariant alpha rho sigma =
  { sigma: iarray alpha } /\ { rho: cell alpha rho sigma }

let mkarray : forall alpha, int * alpha -> array alpha =
lambda (n : int, v : alpha).
  (* Allocate the base array. *)
  let sigma, { sigma : iarray alpha }, (a : [sigma]) = imkarray n v in
  (* Create an initially empty group region for the cells. *)
  new region rho, { rho: cell alpha rho sigma } in
  (* Create a cell that represents the initial array. *)
  let (c : [rho]) = ref (Base a) in
  (* At this point, we hold the capability (invariant alpha rho sigma).
     We now hide it, under the name R. As usual (see the paper), R must
     be recursively defined. This would not be necessary if alpha was a
     base type, such as int. *)
  hide R = (invariant alpha rho sigma) under R outside of
  (* We now hold R. *)
  (* Define a type abbreviation for the internal view of elements.
     Note: if alpha is a base type, such as int, then
     element is just alpha. *)
  def type element =
    alpha under R
  in
  (* Note: R is equal to invariant element rho sigma. *)

  (* Define accessor methods for arrays. Nothing particularly
     interesting goes on here. These are first-order functions.
     Every function requires R and preserves R. *)

  let rec aget : R /\ ([rho] * int) -> R /\ element =
  lambda (c : [rho], i : int).
    (* c is a cell, i is an index *)
    (* We hold R, so we can read/write the data structure. *)
    case get c of
      | Base a ->
	  iget (a, i)
      | Diff (j, v : element, c) ->
	  if i = j then v else aget (c, i)
  in

  let rec reroot : R /\ [rho] -> R /\ unit =
  lambda (c : [rho]).
    case get c of
      | Base _ ->
	  ()
      | Diff (j, v, d) ->
	  reroot d;
	  case get d of
            | Base a ->
		let w = iget (a, j) in
		iset (a, j, v);
		d := Diff (j, w, c);
		c := Base a
	    | _ ->
		assert false
  in

  let rec aset : R /\ ([rho] * int * element) -> R /\ [rho] =
  lambda (c : [rho], i : int, v : element).
    (* c is a cell, i is an index, v is an element *)
    (* Reroot c and extract the base imperative array. *)
    reroot c;
    case get c of
      | Base a ->
	(* Read the current value at i. *)
	let w = iget (a, i) in
	(* Allocate a new cell. *)
	let d : [rho] = ref (Base a) in
	(* Redirect the previous cell. *)
	set (c, Diff (i, w, d));
	(* Update the base array. *)
	iset (a, i, v);
	(* Return the new cell. *)
	d
      | _ ->
	  assert false
  in

  (* Package the accessor functions as an object. This step is made
     necessary by the fact that the types of the accessor functions
     refer to the region variables rho and sigma, which will go out of
     scope when we exit mkarray. To do this, we define a recursive
     function that packages a cell as an array object. *)

  (* Note: (array alpha) under R
         = ((int -> alpha) under R) * ((int * alpha -> array alpha) under R
         = (R /\ int -> R /\ element) * (R /\ (int * element) -> R /\ ((array alpha) under R)) *)

  let rec package : [rho] -> (array alpha) under R =
  lambda (c : [rho]).
    let get : R /\ int -> R /\ element =
    lambda (i : int).
      aget (c, i)
    and set : R /\ (int * element) -> R /\ ((array alpha) under R) =
    lambda (i : int, v : element).
      let d : [rho] = aset (c, i, v) in
      package d
  in

  (* Package the initial array. *)
  (* This expression has type (array alpha) under R within anti-frame,
     so its external type is array alpha. *)

  package c

(* end of mkarray *)

(* Optional: if desired, we can re-package persistent arrays as an
   abstract data type, equipped with mkarray/aget/aset operations.
   mkarray is defined above, so there only remains to define aget
   and aset. This is done via method invocation. *)

let aget : array alpha * int -> alpha =
lambda ((aget, _) : array alpha, i : int).
  aget i

let aset : array alpha * int * alpha -> array alpha =
lambda ((_, aset) : array alpha, i : int, v : alpha).
  aset (i, v)

(* At this point, the type constructor array can be made abstract. *)

effets et ordre supérieur

• author:
• code:
• probleme(s):
  • effets et ordre superieur
  • langage de spec pour de tels programmes
• solution(s)?:

(* quelle spec ? *)
let rec iter f l =
    match l with
    | [] -> ()
    | hd::tl -> f hd; iter f tl

(* quelle spec ? *)
let rec fold_left f acc l =
    match l with
    | [] -> acc
    | hd::tl -> fold_left (f acc hd) tl

Crible

author: Sylvain

//@ ensures "tu vas appeler f successivement sur chacun des nombres
premiers entre 2 et n"

let rec eratosthene (f:int->unit) (n:int) : unit =
  if n=2
  then
    (f 2)
  else
    let prime=ref true in
    eratosthene 
      (fun p -> (if n mod p = 0 then prime:=false); f p)
      (n-1) ;
    if !prime then (f n)

Wrapper liste+longueur

author:Claude

class C { 

  private int n;
  private List<String> l;
  model L;

  // version 1: pas de copie
  // spec: le client n'a pas le droit de modifier \result
  List<String> get1() { return l; }

  // version 2: shallow copie
  // spec: le client a le droit de modifier \result
  List<String> get2() { return l.clone(); }

  void add(String s) { l.add(s); n+=1 }
} 

int main() { 

  C c = new C(3, s1::s2::s3);
  List<String> m = c.get();
  // quelle est la bonne spec pour m ?
  c.add(s4)
  // m.add(s5) doit être interdit
  print(m.length()) // affiche 4
} 

graphe cyclique

Author: Romain

Pour construire un graphe cyclique, en Caml, on a deux possibilités : - utiliser "let rec", mais ça ne marche qu'avec un nombre fini de noeuds ; - utiliser un champ mutable pour créer tous les noeuds, puis remplir ce champ avec les noeuds voisins.

Une fois que le graphe est construit, on peut oublier que le champ était mutable. On pourrait donc vouloir abstraire le type des noeuds pour oublier que le champ est mutable.

C'est un cas particulier simple du cadre plus général des effets cachés, puisqu'ici on n'a aucune fonction autre que le constructeur qui modifie l'objet.

structures auto-réorganisantes

• tableaux persistants [ConchonFilliatre07wml]
• tableaux semi-persistants [ConchonFilliatre08esop]
• splay trees
• union-find imperatif
• union-find persistant
• hash-consing
• typage (destructif) de ML
• preuve du noyau de HOL-light (300 lignes de Caml)
  • defi : exceptions
• Algorithme de Koda-Ruskey [FilliatrePottier02]
  • defi: ordre sup et effet

Raffinement de programmes Java

programmes à pointeurs et modifications en place, munis de modèles algébriques

• renversement d'une liste
• files de priorités

<bibtex> @incollection{marche07,

 topics = {team},
 author = {Claude March\'e},
 title = {Towards Modular Algebraic Specifications for Pointer Programs: a Case Study},
 booktitle = {Rewriting, Computation and Proof},
 pages = {235--258},
 year = 2007,
 editor = {H. Comon-Lundh and C. Kirchner and H. Kirchner},
 volume = 4600,
 series = {Lecture Notes in Computer Science},
 type_digiteo = {chapitre},
 type_publi = {chapitre},
 publisher = {Springer}

} </bibtex>

• tables d'associations implantées par hachage

class FibMemo {

    private HashMap<Integer,Long> memo;

    // invariant \forall Integer x, Long y ; 
    //    (x,y) \in memo.model ==>  y.model = math_fib(x.model)

    FibMemo () {
	memo = new HashMap<Integer,Long>();
    }

    long fib(int n) {       
	if (n <= 1) return 1; 
	Long x = memo.get(n);
	if (x != null) return x.longValue();
	long y = fib(n-1) + fib(n-2);
	memo.put(n,y); return y;
    }
}

• algorithmes de BDD.