September Morn Update

Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-4.spark

@@ -0,0 +1,22 @@
+package Bubble with SPARK_Mode is
+
+   type Arr is array (Integer range <>) of Integer;
+
+   function Sorted (A : Arr) return Boolean is
+     (for all I in A'First .. A'Last - 1 => A(I) <= A(I + 1))
+       with
+         Ghost,
+         Pre => A'Last > Integer'First;
+
+   function Bubbled (A : Arr) return Boolean is
+     (for all I in A'First .. A'Last - 1 => A(I) <= A(A'Last))
+       with
+         Ghost,
+         Pre => A'Last > Integer'First;
+	
+   procedure Sort (A : in out Arr)
+     with
+       Pre => A'Last > Integer'First and A'Last < Integer'Last,
+     Post => Sorted (A);
+	
+end Bubble;

Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-5.spark

@@ -0,0 +1,34 @@
+package body Bubble with SPARK_Mode is
+
+   procedure Sort (A : in out Arr)
+   is
+      Prev : Arr (A'Range) with Ghost;
+      Done : Boolean;
+   begin
+      for I in reverse A'First .. A'Last - 1 loop
+         Prev := A;
+         Done := True;
+         for J in A'First .. I loop
+            if A(J) > A(J + 1) then
+               declare
+                  TMP : Integer := A(J);
+               begin
+                  A(J) := A(J + 1);
+                  A(J + 1) := TMP;
+                  Done := False;
+               end;
+            end if;
+            pragma Loop_Invariant (if Done then Sorted (A(A'First .. J + 1)));
+            pragma Loop_Invariant (Bubbled (A(A'First .. J + 1)));
+            pragma Loop_Invariant (A(J + 2 .. A'Last) = Prev(J + 2 .. A'Last));
+            pragma Loop_Invariant (for some K in A'First .. J + 1 =>
+                                     A(J + 1) = Prev(K));
+         end loop;
+         exit when Done;
+         pragma Loop_Invariant (if Done then Sorted (A));
+         pragma Loop_Invariant (Bubbled (A(A'First .. I + 1)));
+         pragma Loop_Invariant (Sorted (A(I + 1 .. A'Last)));
+      end loop;
+   end Sort;
+
+end Bubble;

Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-6.spark

@@ -0,0 +1,11 @@
+with Ada.Integer_Text_IO;
+with Bubble;
+
+procedure Main is
+   A : Bubble.Arr := (5,4,6,3,7,2,8,1,9);
+begin
+   Bubble.Sort (A);
+   for I in A'Range loop
+      Ada.Integer_Text_IO.Put (A(I));
+   end loop;
+end Main;

Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-7.spark

@@ -0,0 +1,5 @@
+project Bubble is
+
+   for Main use ("main.adb");
+
+end Bubble;