aparler/RosettaCodeData
1
0
Fork 0
Code Issues 12 Pull requests 3 Projects Releases Packages Wiki Activity Actions

all tasks

Browse source
This commit is contained in:
Ingy döt Net 2013-04-11 01:07:29 -07:00
parent b83f433714
commit 68f8f3e56b
14735 changed files with 178959 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

36
Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-1.spark Normal file
View file

@ -0,0 +1,36 @@
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;

49
Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-2.spark Normal file
View file

@ -0,0 +1,49 @@
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
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;

63
Task/Sorting-algorithms-Bubble-sort/SPARK/sorting-algorithms-bubble-sort-3.spark Normal file
View file

@ -0,0 +1,63 @@
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
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 -- I is unchanged by execution of the loop
--# 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;