New example: bubble sort

examples/bubble_sort.mlw

+
+(* {1 Bubble sort} *)
+
+module BubbleSort
+
+  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
+
+
+  let bubble_sort (a: array int)
+    ensures { permut_all (old a) a } 
+    ensures { sorted a }
+  = 'Init:
+    for i = length a - 1 downto 1 do
+      invariant { permut_all (at a 'Init) a }
+      invariant { sorted_sub a i (length a) }
+      invariant { forall k1 k2: int. 
+        0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] 
+      }
+      for j = 0 to i - 1 do
+        invariant { permut_all (at a 'Init) a }
+        invariant { sorted_sub a i (length a) }
+        invariant { forall k1 k2: int. 
+          0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] 
+        }
+        invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
+        if a[j] > a[j+1] then swap a j (j+1);
+      done;
+    done
+
+  let test1 () =
+    let a = make 3 0 in
+    a[0] <- 7; a[1] <- 3; a[2] <- 1; 
+    bubble_sort a;
+    a
+
+  let test2 () ensures { result.length = 8 } =
+    let a = make 8 0 in
+    a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
+    a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
+    bubble_sort a;
+    a
+
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    let a = test2 () in
+    if a[0] <> -5 then raise BenchFailure;
+    if a[1] <> 6 then raise BenchFailure;
+    if a[2] <> 17 then raise BenchFailure;
+    if a[3] <> 42 then raise BenchFailure;
+    if a[4] <> 53 then raise BenchFailure;
+    if a[5] <> 69 then raise BenchFailure;
+    if a[6] <> 91 then raise BenchFailure;
+    if a[7] <> 413 then raise BenchFailure;
+    a
+
+end

examples/bubble_sort/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<file name="../bubble_sort.mlw" expanded="true">
+<theory name="BubbleSort" expanded="true">
+ <goal name="WP_parameter bubble_sort" expl="VC for bubble_sort" sum="dd8e246867c00ac7a35f69a192463155">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter bubble_sort.1" expl="1. postcondition" sum="2367840c905854793a015d90d08abe1c">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.2" expl="2. postcondition" sum="9a1a731b987edcb5a119cb4c4df5ebc5">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.3" expl="3. loop invariant init" sum="780e0aee6090d640b1feade4fa507b46">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.4" expl="4. loop invariant init" sum="8b740252583b6f88714b56dfb1bbe18d">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.5" expl="5. loop invariant init" sum="03f9447c3aa8095c28c1e0dc6a89ab05">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.6" expl="6. loop invariant preservation" sum="30133fd22835a4084873f7c755574617">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.7" expl="7. loop invariant preservation" sum="7bd5882b637ec3f65fcddb64a206d885">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.8" expl="8. loop invariant preservation" sum="45616cc7d63e329ef8629838c8f9c35c">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.9" expl="9. loop invariant init" sum="b39f5223b6be5500e7b34e7d51f8c947">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.10" expl="10. loop invariant init" sum="206c665ccbc3142c6d2391b506dc5a3f">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.11" expl="11. loop invariant init" sum="3854830b0db5e8c9c7b33b204fa5bba1">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.12" expl="12. loop invariant init" sum="dd988ebc57329d4fa31f8f45cf9866e7">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.13" expl="13. type invariant" sum="bd61a719fa85eee86acf9971092a2ac7">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.14" expl="14. index in array bounds" sum="8549dd4bb9f163711608f7a334e8c252">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.15" expl="15. index in array bounds" sum="be06ad66565f19d46135149b6b8a35cc">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.16" expl="16. precondition" sum="6ad1094c5617d5e40789a08c6e88eb78">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.17" expl="17. loop invariant preservation" sum="4e343a548a65756ba5a02753b2c22e93">
+  <proof prover="0"><result status="valid" time="0.17"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.18" expl="18. loop invariant preservation" sum="32fad9b47265c72d834e1da8511dcd31">
+  <proof prover="0"><result status="valid" time="0.22"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.19" expl="19. loop invariant preservation" sum="e55632e11bb877795b2d3c4e060d85d5">
+  <proof prover="0"><result status="valid" time="1.04"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.20" expl="20. loop invariant preservation" sum="149aad01ecdecbd3c20975f5fb6ba9f6">
+  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.21" expl="21. loop invariant preservation" sum="7d7e9f93085cd7f2aea1a241691eb88d">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.22" expl="22. loop invariant preservation" sum="152439613e9a8d3862ca69c4ee3fdde4">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.23" expl="23. loop invariant preservation" sum="7d02d773f5ecc1f2890bcf445d0a2c3a">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.24" expl="24. loop invariant preservation" sum="706599ebbab599f0f86da9cc555fd1ab">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.25" expl="25. loop invariant preservation" sum="0acc8662835ad2e7e47a761df4f7dca4">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.26" expl="26. loop invariant preservation" sum="f9f2eb2aee49eb2132f78d4d9dfcb539">
+  <proof prover="0"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.27" expl="27. loop invariant preservation" sum="a79903d9761be82fd51ad7a2fcb0500d">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.28" expl="28. type invariant" sum="2b4a28b79ac710554d3164f58561c7ac">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.29" expl="29. postcondition" sum="18a0dc072aaba03f02f81bf7aac8027e">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter bubble_sort.30" expl="30. postcondition" sum="764bb11986b65f92828bdce11a837d3d">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter test1" expl="VC for test1" sum="89816521a967170d123b9dcbfc918b70">
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="WP_parameter test2" expl="VC for test2" sum="6719dfeac04f366278fef89fcc7b1deb">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="WP_parameter bench" expl="VC for bench" sum="40340d51311e9da02932248d537f758b">
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>