vault backup: 2023-11-21 23:12:29

.obsidian/app.json

@@ -1,3 +0,0 @@
-{
-  "alwaysUpdateLinks": true
-}

.obsidian/workspace.json

@@ -25,7 +25,7 @@
             "state": {
               "type": "markdown",
               "state": {
-                "file": "4a1s/DAA/PL - Project.md",
+                "file": "4a1s/MFES/PL - Aula 9.md",
                 "mode": "source",
                 "source": false
               }
@@ -98,7 +98,7 @@
             "state": {
               "type": "backlink",
               "state": {
-                "file": "4a1s/DAA/PL - Project.md",
+                "file": "4a1s/MFES/PL - Aula 9.md",
                 "collapseAll": false,
                 "extraContext": false,
                 "sortOrder": "alphabetical",
@@ -115,7 +115,7 @@
             "state": {
               "type": "outgoing-link",
               "state": {
-                "file": "4a1s/DAA/PL - Project.md",
+                "file": "4a1s/MFES/PL - Aula 9.md",
                 "linksCollapsed": false,
                 "unlinkedCollapsed": true
               }
@@ -138,7 +138,7 @@
             "state": {
               "type": "outline",
               "state": {
-                "file": "4a1s/DAA/PL - Project.md"
+                "file": "4a1s/MFES/PL - Aula 9.md"
               }
             }
           },
@@ -173,13 +173,15 @@
   },
   "active": "06edd90495d96c81",
   "lastOpenFiles": [
+    "4a1s/MFES/PL - Aula 8.md",
+    "4a1s/MFES/PL - Aula 9.md",
+    "4a1s/MFES/Untitled",
+    "4a1s/DAA/PL - Project.md",
     "4a1s/DAA/PL - Aula 2.md",
     "4a1s/DAA/PL - Aula 1.md",
-    "4a1s/DAA/PL - Project.md",
     "PL - Aula 9.md",
     "4a1s/CP/PL - Aula 8.md",
     "4a1s/CP/PL - Aula 7.md",
-    "4a1s/MFES/PL - Aula 8.md",
     "4a1s/MFES/PL - Aula 4.md",
     "4a1s/MFES/MFES - UC Details.md",
     "4a1s/MFES/PL - Aula 3.md",
@@ -198,7 +200,6 @@
     "4a1s/CP/PL - Aula 6.md",
     "4a1s/RAS/PL - Aula n.md",
     "Excalidraw/Drawing 2023-10-04 12.19.18.excalidraw.md",
-    "Excalidraw/doodles.excalidraw.md",
     "Images/Pasted image 20231018122801.png",
     "Images/Pasted image 20231018121319.png",
     "Images/Pasted image 20231018120412.png",
@@ -217,7 +218,6 @@
     "-.32118",
     "4a1s/ASCN/T",
     "4a1s/ASCN/T.32118",
-    "4a1s/ASCN/Images.md.32118",
-    "script.sh"
+    "4a1s/ASCN/Images.md.32118"
   ]
 }

4a1s/MFES/PL - Aula 9.md

@@ -0,0 +1,190 @@
+```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