Ada的子项目合同

Question

我正在阅读一份关于Ada编程的文档，更具体地说，Ada用于c++ Java开发人员，或者我遇到麻烦并理解并能够使用文档中给出的一些示例，其中一个是关于前置和后置条件

但是，当我编译该程序时，我刚刚得到一个+Inf****消息-我期望编译失败，因为我试图传递0作为除数。

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;

Answer 1

在ARM 11.4.2(1.1)中，前置条件和后置条件都是断言。GNAT默认不启用断言:您需要通过使用-gnata编译来启用它们。

如果您正在使用gprbuild，您将需要向您的项目添加类似这样的内容。探地雷达文件:

package Compiler is
  for Default_Switches ("Ada") use
    ("-gnata"); -- enable assertions
end Compiler;