The Ada Program: condition.adb

  1 -- condition.adb:  pre- and post-conditions
  2 
  3 with Ada.Text_IO, Ada.Integer_Text_IO, Ada.Exceptions, System.Assertions;
  4 use Ada;
  5 
  6 procedure Condition is
  7 
  8    N,Q: Integer;
  9 
 10 begin
 11 
 12    Read: loop
 13 
 14       -- Get input interactively from user until N<=0
 15       Text_IO.Put ("Enter an integer N:  ");
 16       Integer_Text_IO.Get (N);
 17 
 18       exit Read when N <= 0;
 19 
 20       pragma Assert (N/=0, "N=0");
 21 
 22       Q := 512 / N;
 23 
 24       -- Postcondition is not
 25       --   a) "Q*N=512", because this is integer division
 26       --   b) "Q*N+(512 mod N)=512", because of N<0
 27       pragma Assert (Q*N+(512 rem N)=512, "Q incorrect");
 28 
 29       Integer_Text_IO.Put (Q);
 30       Text_IO.New_Line;
 31 
 32    end loop Read;
 33 
 34 exception
 35    when E:System.Assertions.Assert_Failure =>
 36       Text_IO.Put ("Assertion failure:  ");
 37       Text_IO.Put_Line (Exceptions.Exception_Message (E));
 38 end Condition;