Subprogram contracts in Ada

Question

I'm reading a document on Ada programming to be more specific, Ada for C++ Java developer, or I'm in trouble and to understand and be able to use some of the examples given in the document, one of them is on the preprocessing of data

But, when I compile that program, I just got a +Inf** message

with Ada.Text_IO;
use Ada.Text_IO;

procedure main is

   function Divisao(Left, Right : Float) return Float
   with Pre => Right /= 0.0,
     Post => Divisao'Result * Right < left + 0.0001
     and then Divisao'Result * Right > Left - 0.0001 
   is
   begin
      return Left/Right;
   end Divisao;

begin
   Put_Line(Float'Image(Divisao(10.3,0.0)));
end main;

PS: in the document, have just the function declaration:

function Divisao(Left, Right : Float) return Float
   with Pre => Right /= 0.0,
     Post => Divisao'Result * Right < left + 0.0001
     and then Divisao'Result * Right > Left - 0.0001;

This system preprocessor should not point this error?

Answer 1

By ARM 11.4.2 (1.1), pre- and postconditions are assertions. GNAT doesn’t enable assertions by default: you need to enable them by compiling with -gnata.