MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

Commit b20ee27d by Jean-Christophe Filliâtre

### program example quicksort completed (with one unproved VC)

parent 6632c4a0
 ... ... @@ -7,9 +7,38 @@ module Quicksort clone import array.ArraySorted with type elt = int, logic le = (<=) use import array.ArrayPermut let swap (t:array int) (i:int) (j:int) = { 0 <= i < length t and 0 <= j < length t } let v = t[i] in begin t[i <- t[j]]; t[j <- v] end { exchange t (old t) i j } let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l } = { 0 <= l and r < length t } if l < r then begin let v = t[l] in let m = ref l in label L: begin for i = l + 1 to r do invariant { (forall j:int. l < j <= m -> t[j] < v) and (forall j:int. m < j < i -> t[j] >= v) and permut t (at t L) l r and t[l] = v and l <= m < i } if t[i] < v then begin m := !m + 1; swap t i !m end done; swap t l !m; quick_rec t l (!m - 1); quick_rec t (!m + 1) r end end { (l <= r and sorted_sub t l r and permut t (old t) l r) or (l > r and array_eq t (old t)) } let quicksort (t : array int) = {} () (*(quick_rec t 0 ((array_length_ t)-1))*) quick_rec t 0 (length t - 1) { sorted t and permutation t (old t) } end ... ...
 ... ... @@ -75,8 +75,25 @@ theory ArraySorted logic le elt elt logic sorted_sub (a : t int elt) (l u : int) = forall i1 i2 : int. l <= i1 <= i2 <= u -> le a[i1] a[i2] logic sorted (a : t int elt) = forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2] sorted_sub a 0 (length a - 1) end theory ArrayEq use import int.Int use export ArrayLength logic array_eq_sub (a1 a2 : t int 'a) (l u : int) = forall i:int. l <= i <= u -> a1[i] = a2[i] logic array_eq (a1 a2 : t int 'a) = length a1 = length a2 and forall i:int. 0 <= i < length a1 -> a1[i] = a2[i] end ... ... @@ -120,9 +137,21 @@ theory ArrayPermut forall a1 a2 : t int 'a. forall l u : int. permut a1 a2 l u -> length a1 = length a2 lemma permut_exists : forall a1 a2 : t int 'a. forall l u : int. permut a1 a2 l u -> forall i : int. l <= i <= u -> exists j : int. l <= j <= u and a2[i] = a1[j] logic permutation (a1 a2 : t int 'a) = permut a1 a2 0 (length a1 - 1) use export ArrayEq lemma array_eq_permut : forall a1 a2 : t int 'a. forall l u : int. array_eq_sub a1 a2 l u -> permut a1 a2 l u end theory ArrayRich ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!