Sorting algorithms/Bubble sort: Difference between revisions

=={{header|SPARK}}==

{{works with|SPARK GPL|2010}}

The first version is a minimal SPARK version. It is based on the Ada version, with Integer for both the array index and the array element.

Static analysis of this code shows that it is guaranteed free of any run-time error when called from any other SPARK code.

<lang Ada>package Bubble

is

type Arr is array(Integer range <>) of Integer;

procedure Sort (A : in out Arr);

--# derives A from *;

end Bubble;

package body Bubble

is

procedure Sort (A : in out Arr)

is

Finished : Boolean;

Temp : Integer;

begin

if A'Last /= A'First then

loop

Finished := True;

for J in Integer range A'First .. A'Last - 1 loop

if A (J + 1) < A (J) then

Finished := False;

Temp := A (J + 1);

A (J + 1) := A (J);

A (J) := Temp;

end if;

end loop;

--# assert A'Last /= A'First;

exit when Finished;

end loop;

end if;

end Sort;

end Bubble;

</lang>

The next version has a postcondition to guarantee that the returned array is sorted correctly. This requires the two proof rules that follow the source. The Ada code is identical with the first version.

<lang Ada>package Bubble

is

type Arr is array(Integer range <>) of Integer;

-- Sorted is a proof function with the definition:

-- Sorted(A, From_I, To_I)

-- <->

-- (for all I in Integer range From_I .. To_I - 1 =>

-- (A(I) <= A(I + 1))) .

--

--# function Sorted (A : Arr;

--# From_I, To_I : Integer) return Boolean;

procedure Sort (A : in out Arr);

--# derives A from *;

--# post Sorted(A, A'First, A'Last);

end Bubble;

package body Bubble

is

procedure Sort (A : in out Arr)

is

Finished : Boolean;

Temp : Integer;

begin

--# check A'Last <= A'First -> A'Last = A'First;

if A'Last > A'First then

loop

Finished := True;

for J in Integer range A'First .. A'Last - 1

--# assert Finished -> Sorted(A, A'First, J);

loop

if A (J + 1) < A (J) then

Finished := False;

Temp := A (J + 1);

A (J + 1) := A (J);

A (J) := Temp;

end if;

end loop;

--# assert A'Last /= A'First

--# and (Finished -> Sorted(A, A'First, A'Last));

exit when Finished;

end loop;

end if;

end Sort;

end Bubble;

</lang>

The proof rules are stated here without justification (but they are fairly obvious). A formal proof of these rules from the definition of Sorted has been completed.

<pre>

bubble_sort_rule(1): sorted(A, I, J)

may_be_deduced_from

[ J <= I ] .

bubble_sort_rule(2): Fin -> sorted(A, I, J + 1)

may_be_deduced_from

[ Fin -> sorted(A, I, J),

element(A, [J]) <= element(A, [J + 1]) ] .

</pre>