97 lines
3.3 KiB
Text
97 lines
3.3 KiB
Text
package Binary_Searches is
|
|
|
|
subtype Item_Type is Integer; -- From specs.
|
|
subtype Index_Type is Integer range 1 .. 100;
|
|
type Array_Type is array (Index_Type range <>) of Item_Type;
|
|
|
|
procedure Search (Source : in Array_Type;
|
|
Item : in Item_Type;
|
|
Found : out Boolean;
|
|
Position : out Index_Type);
|
|
--# derives Found,
|
|
--# Position from
|
|
--# Source,
|
|
--# Item;
|
|
--# post Found -> Source (Position) = Item;
|
|
-- If Found is False then Position is undefined.
|
|
|
|
end Binary_Searches;
|
|
|
|
|
|
package body Binary_Searches is
|
|
|
|
procedure Search (Source : in Array_Type;
|
|
Item : in Item_Type;
|
|
Found : out Boolean;
|
|
Position : out Index_Type)
|
|
is
|
|
Lower : Index_Type; -- Lower bound of Subrange.
|
|
Upper : Index_Type; -- Upper bound of Subrange.
|
|
Terminated : Boolean;
|
|
begin
|
|
Found := False;
|
|
-- Default status updated on success.
|
|
|
|
Lower := Source'First;
|
|
Upper := Source'Last;
|
|
Position := (Lower + Upper) / 2;
|
|
Terminated := False;
|
|
|
|
while not Terminated loop
|
|
--# assert Lower >= Source'First
|
|
--# and Upper <= Source'Last
|
|
--# and Position in Lower .. Upper
|
|
--# and not Found;
|
|
if Item < Source (Position) then
|
|
if Position = Lower then
|
|
-- No lower subrange.
|
|
Terminated := True;
|
|
else
|
|
--# check Position > Lower;
|
|
-- For the two following proofs.
|
|
|
|
--# check Position - 1 >= Lower;
|
|
--# check Lower + Position - 1 >= Lower * 2;
|
|
--# check (Lower + Position - 1) / 2 >= Lower;
|
|
-- For "Position >= Lower" in loop assertion.
|
|
|
|
--# check Lower < Position;
|
|
--# check Lower + Position - 1 <= (Position - 1) * 2;
|
|
--# check (Lower + Position - 1) / 2 <= (Position - 1);
|
|
-- For "Position <= Upper" in loop assertion.
|
|
|
|
-- Switch to lower half subrange.
|
|
Upper := Position - 1;
|
|
Position := (Lower + Upper) / 2;
|
|
end if;
|
|
|
|
elsif Item > Source (Position) then
|
|
if Position = Upper then
|
|
-- No upper subrange.
|
|
Terminated := True;
|
|
else
|
|
--# check Position < Upper;
|
|
-- For the two following proofs.
|
|
|
|
--# check Upper >= Position + 1;
|
|
--# check Position + 1 + Upper >= (Position + 1) * 2;
|
|
--# check (Position + 1 + Upper) / 2 >= (Position + 1);
|
|
-- For "Position >= Lower" in loop assertion.
|
|
|
|
--# check Position + 1 <= Upper;
|
|
--# check Position + 1 + Upper <= Upper * 2;
|
|
--# check (Position + 1 + Upper) / 2 <= Upper;
|
|
-- For "Position <= Upper" in loop assertion.
|
|
|
|
-- Switch to upper half subrange.
|
|
Lower := Position + 1;
|
|
Position := (Lower + Upper) / 2;
|
|
end if;
|
|
else
|
|
Found := True;
|
|
Terminated := True;
|
|
end if;
|
|
end loop;
|
|
end Search;
|
|
|
|
end Binary_Searches;
|