Module certification

Dans ce TD, on certifie plusieurs programmes vérifiant qu'un tableau d'entiers est trié de manière croissante et retournant, dans le cas négatif, un indice du tableau où l'inégalité n'est pas satisfaite.

Programmes fonctionnels

Dans cette première partie, on s'intéresse à des programmes fonctionnels, et des tableaux représentés par des fonctions de type nat->nat.

Definition array := nat -> nat.

Fonction récursive + preuve. Écrire une fonction is_sorted prenant en arguments t:array, m:nat et retournant une valeur de type (option nat) valant None si le tableau t[0]...t[m] est trié de manière croissante et (Some i) avec 0 <= i < m si t[i] > t[i+1].

Require Arith.
Require Compare_dec.

Fixpoint is_sorted [t:array; m:nat] : (option nat) :=
  Cases m of
  | O =>
      (None nat)
  | (S m') =>
      if (le_gt_dec (t m') (t m)) then [_](is_sorted t m') else [_](Some nat m')
  end.

Definition sorted :=
  [t:array][m:nat](i:nat)(le O i) -> (lt i m) -> (le (t i) (t (S i))).

Lemma is_sorted_correct :
  (t:array)(m:nat)Cases (is_sorted t m) of
                    | None => (sorted t m)
                    | (Some i) => (gt (t i) (t (S i))) end.
Proof.
Induction m; Simpl.
Unfold sorted; Intros; Absurd (le O i); Auto with arith.
Intros m'; Case (le_gt_dec (t m') (t (S m'))); Auto.
Case (is_sorted t m'); Auto.
Unfold sorted; Intros.
Case (le_lt_eq_dec i m'); Auto with arith.
Intro Hi; Rewrite Hi; Auto.
Save.

Extraction

Écrire un type inductif correspondant à la spécification de is_sorted.

Inductive is_sorted_spec [t:array; m:nat] : Set :=
  | Sorted : (sorted t m) -> (is_sorted_spec t m)
  | Unsorted : (i:nat)(gt (t i) (t (S i))) -> (is_sorted_spec t m).

L'extraction de ce type inductif doit être isomorphe à option nat

Extraction is_sorted_spec.

Montrer directement cette spécification et extraire le programme.

Lemma is_sorted_2 : (t:array)(m:nat)(is_sorted_spec t m).
Proof.
Induction m.
Apply Sorted; Unfold sorted; Intros; Absurd (le O i); Auto with arith.
Intros n Hn; Case (le_gt_dec (t n) (t (S n))); Intro.
Elim Hn; Unfold sorted; Intros.
Apply Sorted; Unfold sorted; Intros.
Case (le_lt_eq_dec i n); Auto with arith.
Intro Hi; Rewrite Hi; Auto.
Apply Unsorted with i; Auto.
Apply Unsorted with n; Auto.
Save.

Extraction is_sorted_2.

Programmes impératifs

Le tableau est maintenant un tableau global au sens de Correctness, donc indexés par le type Z. Sa taille est un paramètre N.

Require Correctness.
Require Omega.

Parameter N : Z.
Axiom N_strictement_positif : `N >= 1`.

Global Variable t : array N of Z.

La spécification du programme impératif est maintenant la suivante : il retourne un booléen indiquant si le tableau est trié ; lorsque ce booléen vaut false, une variable globale index désigne un indice du tableau où l'inégalité n'est pas satisfaite.

Global Variable index : Z ref.

Definition Zsorted :=
  [t:(array N Z)](i:Z)`0 <= i < N-1` -> `(access t i) <= (access t (i+1))`.

Definition is_sorted_imp_spec :=
  [t:(array N Z)][r:bool][i:Z]
  if r then (Zsorted t) else `(access t i) > (access t (i+1))`.

Premier programme impératif avec une boucle while. La recherche est effectuée de haut en bas avec un indice i ; on sort de la boucle lorsque i vaut -1. Déterminer l'invariant de boucle, le variant, et établir les obligations de preuve.

Correctness is_sorted_3
  (let i = ref (N-2) in
   begin
     index := (Zopp 1);
     while !i >= 0 do
       { invariant
           `-1 <= i < N-1` /\
           ((`index = -1` /\
              (j:Z)`i < j < N-1` -> `(access t j) <= (access t (j+1))`) \/
           (`index >= 0` /\ `(access t index) > (access t (index+1))`))
         variant `i+1`
       }
       if t[!i] <= t[!i+1] then
         i := !i - 1
       else begin
         index := !i;
         i := (Zopp 1)
       end
     done;
     !index = (Zopp 1)
   end)
  { (is_sorted_imp_spec t result index) }.
Proof.
Omega.
Omega.
Repeat Split; Try Omega.
Intuition.
Left. Split. Assumption.
Intros; Case (Z_le_lt_eq_dec i0 j).
Omega.
Intro; Apply H3; Omega.
Intro Hj; Rewrite <- Hj; Assumption.
Repeat Split; Try Omega.
Intuition.
Split. Generalize N_strictement_positif; Omega.
Left. Split. Trivial.
Intros; Absurd `N-2 < j < N-1`; Omega.
Decompose [and or] Post8; Clear Post8;
  Unfold is_sorted_imp_spec; Induction result0.
Unfold Zsorted; Intros; Apply H4; Omega.
Absurd `index1 = -1`; Omega.
Absurd `index1 = -1`; Omega.
Assumption.
Save.

Deuxième programme impératif, avec cette fois une fonction récursive. Déterminer les pré- et post-conditions de la fonction check et établir les obligations de preuve.

Correctness is_sorted_4
 (let rec check (i:Z) : bool { variant `i+1` } =
   { `-1 <= i < N-1` /\
     (j:Z)`i < j < N-1` -> `(access t j) <= (access t (j+1))` }
   (if i = (Zopp 1) then
      true
    else if t[i] > t[i+1] then begin
      index := i;
      false
    end else
      (check (i-1)))
    { if result then (Zsorted t)
                else `(access t index) > (access t (index+1))` }
  in
  check (N-2))
  { (is_sorted_imp_spec t result index) };
Try Clear vf; Try Clear check.
Proof.
Split. Generalize N_strictement_positif; Omega.
Intros; Absurd `N-2 < j < N-1`; Omega.
Decompose [and] Pre3.
Unfold Zsorted; Intros; Apply H0; Omega.
Omega.
Omega.
Unfold Zwf; Omega.
Split.
Omega.
Decompose [and] Pre3; Clear Pre3.
Intros; Case (Z_le_lt_eq_dec i0 j). Omega.
Intro; Apply H0; Omega.
Intro Hj; Rewrite <- Hj; Assumption.
Save.