my_digital_garden/4a1s/MFES/PL - Aula 9.md

```c

(* 
    Write appropriate definitions and specifications for
    functions split and merge, used by the merge sort 
    algorithm defined below in the module. 
    
    Note that the verification of mergesort relies only 
    on the specifications ("contracts") of the auxiliary 
    functions, and not on their code. As such, it is crucial
    to include in them every aspect required for the
    verification conditions of the sorting algorithm
    to be successfully discharged.
    
    Note also that although Why3 is capable of automatically 
    proving the termination of functions with simple recursive
    patterns, that does not apply to the mergesort function. 
    We thus include in the contract the variant "length l", 
    which is valid since the function is recursively called 
    on lists that are shorter than l. 
*)    



module MergeSort

  use int.Int
  use list.List
  use list.Length
  use list.Permut
  use list.Append
  use list.SortedInt



  let rec function split (l :list int) : (list int, list int)
    ensures { let (l1, l2) = result in permut l (l1++l2) }
    ensures {let (l1,l2) = result in length l<2 || (length l>=2 && 
        length l1<length l2 && length l2 < length l1)}
  = match  l with 
        | Nil -> (Nil, Nil)
        | Cons x Nil -> (l, Nil)
        | Cons x (Cons y t) -> let (l1, l2) = split t
            in (Cons x l1, Cons y l2) 
  end



  let rec function merge (l1 l2 :list int) : list int
    requires { sorted l1 && sorted l2 }
    ensures  { sorted result} 
    ensures {permut result (l1++l2)}
  = match l1, l2 with
    Nil, _ -> l2
    | _, Nil -> l1
    | (Cons x l1'), (Cons y l2') -> if x<=y
        then Cons x (merge l1' l2)
        else Cons y (merge l1 l2')
  end


  
  let rec function mergesort (l :list int)
    ensures { sorted result } 
    ensures { permut l result } 
    variant { length l }
  =
    match l with
    | Nil -> Nil
    | Cons x Nil -> Cons x Nil
    | _ ->   let (l1,l2) = split l
             in merge (mergesort l1) (mergesort l2)
    end




  predicate is_a_sorting_algorithm (f: list int -> list int) = 
    forall al :list int. permut al (f al) /\ sorted (f al)

  goal is_a_sorting_algorithm : is_a_sorting_algorithm mergesort



end
```


```c

(* 
    The selection sort algorithm sorts an array 
    by successively placing in each position the 
    “next minimum” element, as follows:

    [40, 20, 10, 30, 60, 0, 80]
    [0, 20, 10, 30, 60, 40, 80]
    [0, 10, 20, 30, 60, 40, 80]
    [0, 10, 20, 30, 60, 40, 80]
    [0, 10, 20, 30, 60, 40, 80]
    [0, 10, 20, 30, 40, 60, 80]
    [0, 10, 20, 30, 40, 60, 80]
    [0, 10, 20, 30, 40, 60, 80]

 1. Complete the contract of function swap, writing 
    adequate pre- and post-conditions.
    Recall that "length a" gives you the allocated length
    of array a.
 2. Write a contract for function select. 
    Write also one or more loop invariants that allow
    you to prove the correctness of the function. 
    Note that a loop variant is not required, since 
    "for" loops are bounded. 
 3. Write one or more loop invariants that allow you to prove
    the correctness of selection_sort_1. 
    You may need to modify the contract of select in order 
    for the loop invariant of selection_sort_1 to be proved. 
 4. Finally, write the algorithm selection_sort_2, which does
    not use the function select. It will have a nested loop; 
    write invariants for both loops and prove the correctness
    of the algorithm. 
*)     


module SelectionSort

  use int.Int
  use ref.Ref
  use array.Array
  use array.IntArraySorted
  use array.ArrayPermut
  use array.ArrayEq



  let swap (a: array int) (i: int) (j: int) 
    requires { 0 <= i< length a && 0 <= j< length a }
    ensures  { (old a)[i] = a[j] && (old a)[j] = a[i] }
    ensures  { forall k:int. 0<=k<length a -> k<>i -> k<>j -> (old a)[i] = a[j]}
    ensures  { permut_all (old a) a }
  = let v = a[i] in
    a[i] <- a[j];
    a[j] <- v



  (* returns the index of a  minimum of 
     the segment of a between indexes i and length a -1. 
   *)
  let select (a: array int) (i: int) : int
    requires { 0 <= i < length a}
    ensures  { i <= result < length a }
    ensures  { forall k:int. 0<=k<length a -> a[result] <= a[k]}
  = let ref min = i in
      for j = i + 1 to length a - 1 do
        invariant { i <= min < j }
        invariant { forall k:int. i <= k < j -> a[min] <= a[k] }
        if a[j] < a[min] then min <- j
      done;
    min


       
  let selection_sort_1 (a: array int) 
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = for i = 0 to length a - 1 do
      invariant { sorted_sub a 0 i }
      invariant { forall k1 k2:int. 0<= k1<i<=k2<length a -> a[k1]<=a[k2]}
      invariant { permut_all (old a) a }
      let min = select a i
      in if min <> i then swap a min i
    done


  let selection_sort_2 (a: array int) =
    ensures { sorted a }
    ensures { permut_all (old a) a }
  ...


end      
```



https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpBJ1Theyselection%2F2sortyalgorithm%2F3sorts0an3arrayBH0byysuccessively%2F5placing0in2each6position1theBH%2Fi%2BA%2Bc2next5minimum%2Fi%2BA%2BdB5element7r0as5follows7vNH72040o020s010s030s060sz0s08074HkpplslslslskskkHkkplskskskskskkHkkpkskskskskskkHkkpkskskskskskkHkkpkskskslskskkHkkpkskskskskskkHkkpkskskskskskkNEz17t6Completea6contract0of6function2swapj5writingBK6adequate1preA7s1and2postArAyconditions%2FfH4Recall2that7h4lengthzar3gives1youZyallocated%2FnHZuHliEz2s3WriteqV1forU4selectnBKn2also1one0or2more2loopyinvariants%2FX3allowHY0to3proveWycorrectness%2FXrcdBH2NotejYg5variant0is1not6required7r3sinceBH7hSs3loops1are5boundedeBEz3sPQQQcQZQQQQKSQQyselection%2Bsort%2B1%2FeBH1You1may2needk4modifykulkuluK3orderBHQnZyinvariant%2Fmei0be4provedcBEz4s5Finally7r3writehuEyselection%2Bsort%2B2%2Fp3which2doesKuo1usemukWh0It2will2haveza4nestedU7wBHbuwR2bothupubuxcuxHu5rTbBN7JoCCBNNN4moduleySelectionSort%2FNFV1intoA1IntHq1refqA1RefHquhqA3ArrayHqqqAyIntArraySorted%2FHqqqyArrayPermut%2FHqqq5ArrayEqNNNH1letuX7nO7vme7ooziopppzjpppBJ6requires77z07RykA7xufg7FlnnhAnnn79H5ensuresCje1oldo7I2g747ypA72gpdkknknnlpAlkphHhCh4forallzkXAXSBYAYAoYAYe7MzpA7RzAdqqAqAaqXXmXlZXpAXk7Y9HXCXypermut%2Ball%2FhhlSsUFiPzvrpAgeeuzJpppp7Rsppc7YwHqqqookNNNFuA5returnsvN3indexvMjCuLrBKp5segmentrp5between5indexesdvIvdoB7sAz17tBFvLGUu9Pm7vvVvY7oofopprrJvV77z0vXmB7xbhA79HvbClnm4resultBllllHlClvWzkfAfYBfAgAoAhAhhvXs72e74lpplvYF7yUvN1minqXvZLvEzjpp7qz1u0aeB7sBp0doJuyQkZeBVfBOHmmPXPAPPBhhoBiiQcSeRlpplpdH0ifookojppkp2thenrvXmF2done7wFpNNKMBvouy7niYviX7oBJvjT4sortedmYHppvTjvTnlsmF7yvlQrz0vlvlm7sz1vlLvldysorted%2Bsub%2FnkigHnnvl0k10k2UAV7tjAvmnA7xAhAqAlAqAbfvls72l7YRyAqqmviHccQQQlQsXHvpvoPvfoYHvivinBvRBpvhvPmopFvhNNNNNFiu1dn7vvhvobcJviXvhlYHppWiWnksmF7NNtNNN1endCCCNN


https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpBJ3Writeyappropriate%2Fydefinitions%2F1andyspecifications%2F1forHyfunctions%2F3splitp3merge7r2used0by1thep2sortBHyalgorithm%2F5defined3below0inn4module7tBHH2Note2thatpyverification%2F0ofymergesort%2F4relies2onlyBH0onnV7Hhycontracts%2F7Bokoyauxiliary%2FBHSUT1noti3their2codeZ0As2suchl0it0is5crucialH0to5includeQ2them3every4aspect6requireduEXHOyconditions%2FUq5sortinguJHg0beysuccessfully%2Fydischarged%2FWHHuM2alsouM6although2Why3V5capableeyautomatically%2FBH5provingcytermination%2FpuU2with4simpleyrecursive%2FH6patterns7re2doesuV3applyUguM6functionVBH0We2thusububm6contracts5variant7h4lengthzl7BrBH3whichO3valid3sincekdpyrecursively%2F4calledBHuU3listsT1are5shorter2thaneVBN7JoCCNNNNuLyMergeSort%2FNF1use1intoA1IntHq2listqA2ListHqqqA4LengthHqqqA4PermutHqqq4AppendHqqqySortedInt%2FNNNH1let1recUuE7nbB7vAkd7oqopp7rrroJ5ensures77hm0l1l0l2m7y4resultu64permutekkA7KqAkk79HffAfllfAllfffu8fA7xAz27c8hooA7TyAo7FlBLpfAlArgprrBqBrp7I9MBg3matchCjuuBMH781Nil7MzerZsZHo2ConszxpmmklplHlllmrzyztnjUndiandvVkLUlhgjjqgiiBMB1endNNNHgvTvTuGhilB7vAvSvSiqBqqJ6requires774sortedlvYrk79HvUCnBpvUApBHppAvSpfkAvSAkvVFQvVoTovVJvVqz%2BvVoH78qpoomHohOzxp7GIrppzyi7Gok0ifkA7RyAnL2thenlpkvbhA7mBh7oH2elseljlllmfMBvXNNHHvXvXvXu0kzl7vvWvWcJvZ77vYvZ79BHppvYjoBoBHu4ovSopF7yJvYqvYH78vYvZsHrPzxqpqqqHpz%2BoCBTWP7rAOWevSeMMvSvbkPjlqqkqMDvcNNNNFypredicate%2Fyis%2Ba%2Bsorting%2Balgorithm%2FnzfA7vvevearrkcBJ4forall0almnn7tBvgoiirj7O3veooooNF2goaleBhsaNNNNb