why3.mlw

module TriEx1
  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArraySwap
  use import array.ArrayPermut
  use import array.ArrayEq


 (* Prédicats et sous-programme utiles (et vus au cours 3) *)
 (*
  predicate sorted (a : array int)

  predicate sorted_sub (a : array int) (i j : int)

  predicate permut_all (a1 a2: array 'a) =
    permut a1 a2

  let swap (a: array int) (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
    a[i] <- a[j];
    a[j] <- v
*)

let minimum (t:array int) (m n:int) : int
  requires { 0 <= m < t.length && 0 <= n < t.length }
=
  let indiceMinimum = ref m in
  for i = m to n-1 do
    invariant { m <= i <= n }
    invariant { m <= !indiceMinimum <= n }
    if t[!indiceMinimum] > t[i] then
      indiceMinimum := i;
  done;
  !indiceMinimum

let tri_selection (t: array int) : unit
  ensures { permut_all t (old (t))}
  ensures { sorted t }
=
  for i = 0 to t.length - 1 do
    invariant { 0 <= i <= t.length }
    invariant { sorted_sub t 0 i }
    swap t i (minimum t i t.length)
  done


  let test1 () =
    let t = make 3 0 in
    t[0] <- 7; t[1] <- 3; t[2] <- 1;
    tri_selection  t;
    assert { t [0] = 1 };
    assert { t [1] = 3 };
    assert { t [2] = 7 };
    t

  let test2 () ensures { result.length = 6 } =
    let t = make 6 0 in
    t[0] <- 53; t[1] <- 91; t[2] <- 17; t[3] <- -5;
    t[4] <- 413; t[5] <- 42;
    tri_selection  t;
    assert { t[0] = -5 };
    assert { t[1] = 17 };
    assert { t[2] = 42 };
    assert { t[3] = 53 };
    assert { t[4] = 91 };
    assert { t[5] = 413 };
    t

end

module TriEx2
  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq
(*
 let tri_insertion (t: array int) : unit
    ensures { permut_all t (old t)}
    ensures { sorted t }
  =
  for i = 0 to t.length -1 do
    invariant { 0 <= i <= t.length -1 }
    invariant { sorted_sub t 0 i }
    let x = t[i];
    let j = i;
    while j > 0 && t[j-1] > x  do
      invariant { 0 < j <= i }
      t[j] <- t[j-1];
      j := !j-1;
    done;
    t[j] <- x;
  done;
*)
end