Contact English version

L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à jour sur notre équipe.

Dijkstra's national flag

Dijkstra's national flag consists in sorting an array containing only three values (namely Blue, White and Red).


Auteurs: Jean-Christophe Filliâtre

Catgories: Sorting Algorithm

Outils: Why3

index



Dijkstra's "Dutch national flag"


module Flag

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut

  type color = Blue | White | Red

  predicate monochrome (a:array color) (i:int) (j:int) (c:color) =
    forall k:int. i <= k < j -> a[k]=c

  let swap (a:array color) (i:int) (j:int) =
      requires { 0 <= i < length a /\ 0 <= j < length a }
      ensures { exchange (old a) a i j }
    let v = a[i] in
    begin
      a[i] <- a[j];
      a[j] <- v
    end

  let dutch_flag (a:array color) (n:int) =
      requires { 0 <= n /\ length a = n }
      ensures { exists b:int. exists r:int.
          monochrome a 0 b Blue /\
          monochrome a b r White /\
          monochrome a r n Red }
      ensures { permut (old a) a }
    let b = ref 0 in
    let i = ref 0 in
    let r = ref n in
'Init:
    while !i < !r do
       invariant { 0 <= !b <= !i <= !r <= n }
       invariant { monochrome a 0  !b Blue }
       invariant { monochrome a !b !i White }
       invariant { monochrome a !r n  Red }
       invariant { length a = n }
       invariant { invarord2"t3mut_sword2">invome_1 linvariant invariantsurchrayPermut[!keyword2">in
    
invariantinvariantdone class="kword2">invariantEnglishzip"/>download ZIPut
chiven class="why"content"ontent">