Anonymous user
Sorting algorithms/Bubble sort: Difference between revisions
→{{header|SPARK}}
m (→version 3, random integers, horizontal list, with interim plots: elided a stray character.) |
|||
Line 4,769:
element(A1, [J + 1]) > element(A1, [J + 2]),
swapped(A1, A2, J + 1, J + 2) ] .
</pre>
{{works with|SPARK GPL|2018}}
File '''bubble.ads''':
<lang ada>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;
</lang>
File '''bubble.adb''':
<lang ada>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;
</lang>
File '''main.adb''':
<lang ada>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;
</lang>
File '''bubble.gpr''':
<lang ada>project Bubble is
for Main use ("main.adb");
end Bubble;
</lang>
To verify the program, execute the command: '''gnatprove -P bubble.gpr -j0 --level=2'''
File '''gnatprove/gnatprove.out''':
<pre>Summary of SPARK analysis
=========================
--------------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved
--------------------------------------------------------------------------------------------------------------------
Data Dependencies . . . . . . .
Flow Dependencies . . . . . . .
Initialization 6 6 . . . . .
Non-Aliasing . . . . . . .
Run-time Checks 36 . . . 36 (CVC4) . .
Assertions 14 . . . 14 (CVC4 64%, Z3 36%) . .
Functional Contracts 7 . . . 7 (CVC4 89%, Z3 11%) . .
LSP Verification . . . . . . .
--------------------------------------------------------------------------------------------------------------------
Total 63 6 (10%) . . 57 (90%) . .
Analyzed 2 units
in unit bubble, 4 subprograms and packages out of 4 analyzed
Bubble at bubble.ads:1 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
Bubble.Bubbled at bubble.ads:11 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (3 checks)
Bubble.Sort at bubble.ads:17 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (50 checks)
Bubble.Sorted at bubble.ads:5 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (4 checks)
in unit main, 0 subprograms and packages out of 1 analyzed
Main at main.adb:4 skipped
</pre>
| |||