Anonymous user
Sorting algorithms/Bubble sort: Difference between revisions
→{{header|SPARK}}: Added third version of procedure, with proof rules.
(Added SPARK implementation of bubble sort) |
(→{{header|SPARK}}: Added third version of procedure, with proof rules.) |
||
Line 1,885:
=={{header|SPARK}}==
{{works with|SPARK GPL|2010}}
The first version 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.
Line 1,925 ⟶ 1,926:
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
Line 1,989 ⟶ 1,988:
[ Fin -> sorted(A, I, J),
element(A, [J]) <= element(A, [J + 1]) ] .
</pre>
Both of the two versions above use an inner loop that scans over all the array on every pass of the outer loop. This makes the proof in the second version very simple.
The final version scans over a reducing portion of the array in the inner loop, consequently the proof becomes more complex. The package specification for this version is the same as the second version above. The package body defines two more proof functions.
<lang Ada>package body Bubble
is
procedure Sort (A : in out Arr)
is
Finished : Boolean;
-- In_Position is a proof function with the definition:
-- In_Position(A, A_Start, A_I, A_End)
-- <->
-- ((for all K in Integer range A_Start .. A_I - 1 =>
-- (A(K) <= A(A_I)))
-- and
-- Sorted(A, A_I, A_End) .
--
--# function In_Position (A : Arr;
--# A_Start, A_I, A_End : Integer) return Boolean;
-- Swapped is a proof function with the definition:
-- Swapped(A_In, A_Out, I1, I2)
-- <->
-- (A_Out = A_In[I1 => A_In(I2); I2 => A_In(I1)]).
--
--# function Swapped (A_In, A_Out : Arr;
--# I1, I2 : Integer) return Boolean;
procedure Swap (A : in out Arr;
I1 : in Integer;
I2 : in Integer)
--# derives A from *, I1, I2;
--# pre I1 in A'First .. A'Last
--# and I2 in A'First .. A'Last;
--# post Swapped(A~, A, I1, I2);
is
Temp : Integer;
begin
Temp := A(I2);
A(I2) := A(I1);
A(I1) := Temp;
end Swap;
pragma Inline (Swap);
begin
--# check A'Last <= A'First -> A'Last = A'First;
if A'Last > A'First then
for I in reverse Integer range A'First + 1 .. A'Last loop
Finished := True;
for J in Integer range A'First .. I - 1 loop
if A (J + 1) < A (J) then
Finished := False;
Swap (A, J, J + 1);
end if;
--# assert I% = I
--# and (for all K in Integer range A'First .. J =>
--# (A(K) <= A(J + 1)))
--# and (I < A'Last -> In_Position(A, A'First, I + 1, A'Last))
--# and (Finished -> Sorted(A, A'First, J + 1));
end loop;
exit when Finished;
--# assert In_Position(A, A'First, I, A'Last);
end loop;
end if;
end Sort;
end Bubble;
</lang>
Completion of the proof of this version requires more rules than the previous version and they are rather more complex. Creation of these rules is quite straightforward - I tend to write whatever rules the Simplifier needs first and then validate them afterwards. A formal proof of these rules from the definition of Sorted, In_Position and Swapped has been completed.
<pre>bubble_sort_rule(1): sorted(A, I, J)
may_be_deduced_from
[ J <= I ] .
bubble_sort_rule(2): sorted(A, I - 1, J)
may_be_deduced_from
[ sorted(A, I, J),
element(A, [I - 1]) <= element(A, [I]) ] .
bubble_sort_rule(3): Fin -> sorted(A, I, J + 1)
may_be_deduced_from
[ Fin -> sorted(A, I, J),
element(A, [J]) <= element(A, [J + 1]) ] .
bubble_sort_rule(4): sorted(A, Fst, Lst)
may_be_deduced_from
[ sorted(A, Fst, I),
I < Lst -> in_position(A, Fst, I + 1, Lst),
I <= Lst ] .
bubble_sort_rule(5): in_position(A, Fst, I, Lst)
may_be_deduced_from
[ I < Lst -> in_position(A, Fst, I + 1, Lst),
for_all(K : integer, Fst <= K and K <= I - 1
-> element(A, [K]) <= element(A, [I])),
I >= Fst,
I <= Lst ] .
bubble_sort_rule(6): I < Lst -> in_position(A2, Fst, I + 1, Lst)
may_be_deduced_from
[ I < Lst -> in_position(A1, Fst, I + 1, Lst),
swapped(A1, A2, J + 1, J + 2),
J + 2 < I + 1,
J >= Fst ] .
bubble_sort_rule(7): I - 1 < Lst -> in_position(A2, Fst, I, Lst)
may_be_deduced_from
[ in_position(A1, Fst, I, Lst),
swapped(A1, A2, J, J + 1),
J + 1 < I,
J >= Fst ] .
bubble_sort_rule(8): for_all(K : integer, I <= K and K <= I
-> element(A, [K]) <= element(A, [I + 1]))
may_be_deduced_from
[ element(A, [I]) <= element(A, [I + 1]) ] .
bubble_sort_rule(9): for_all(K : integer, I <= K and K <= I
-> element(A2, [K]) <= element(A2, [I + 1]))
may_be_deduced_from
[ element(A1, [I]) > element(A1, [I + 1]),
swapped(A1, A2, I, I + 1) ] .
bubble_sort_rule(10): for_all(K2 : integer, Fst <= K2 and K2 <= J + 1
-> element(A, [K2]) <= element(A, [J + 2]))
may_be_deduced_from
[ for_all(K1 : integer, Fst <= K1 and K1 <= J
-> element(A, [K1]) <= element(A, [J + 1])),
element(A, [J + 1]) <= element(A, [J + 2]) ] .
bubble_sort_rule(11): for_all(K2 : integer, Fst <= K2 and K2 <= J + 1
-> element(A2, [K2]) <= element(A2, [J + 2]))
may_be_deduced_from
[ for_all(K1 : integer, Fst <= K1 and K1 <= J
-> element(A1, [K1]) <= element(A1, [J + 1])),
element(A1, [J + 1]) > element(A1, [J + 2]),
swapped(A1, A2, J + 1, J + 2) ] .
</pre>
| |||