package pkg is
   function Sqrt (Arg : Integer) return Integer;
   pragma Precondition (Arg >= 0);
   pragma Postcondition
     (Sqrt'Result >= 0
      and then
        (Sqrt'Result ** 2) <= Arg
      and then
        (Sqrt'Result + 1) ** 2 > Arg);
end pkg;
with pkg; use pkg;
with Text_IO; use Text_IO;
procedure Main is
begin
   Put_Line (Sqrt (9)'Img);
   Put_Line (Sqrt (10)'Img);
   Put_Line (Sqrt (-3)'Img);
end;
package body pkg is
   function Sqrt (Arg : Integer) return Integer is
      Result : Integer := 0;
   begin
      loop
         Result := Result + 1;
         if Result ** 2 > Arg then
            return Result;
         end if;
      end loop;
   end;
end pkg;