gnatprove_11.2.3_f7ece6d3/share/examples/spark/spark_book/Chapter-03/bingo_basket_test.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
with Bingo_Numbers;  use Bingo_Numbers;
with Bingo_Basket;
with Ada.Text_IO; use Ada.Text_IO;
procedure Bingo_Basket_Test is

   package Bingo_Number_IO is new Ada.Text_Io.Integer_Io (Bingo_Number);
   use Bingo_Number_IO;

   package Letter_IO is new Ada.Text_Io.Enumeration_Io (Bingo_Letter);
   use Letter_IO;

   Number : Callable_Number;
   Letter : Bingo_Letter;
begin
   Bingo_Basket.Load;
   while not Bingo_Basket.Empty loop
      Bingo_Basket.Draw (Letter => Letter,
                         Number => Number);
      Put (Letter);
      Put (Item => Number,
           Width => 3);
      New_Line;
   end loop;
end Bingo_Basket_Test;