1

我对 Ada 还是有点陌生​​，我想我误解了先决条件的使用，因为通过 GNAT RM 看起来检查似乎不是在运行时执行的。此外，这里的前提条件的 GNAT RM没有指定如果不满足前提条件则抛出哪个异常。

这是我正在尝试的代码：

procedure Test is
begin

   generic
      type Element_Type is private;
      use System.Storage_Elements;
   procedure Byte_Copy (Destination : out Element_Type;
                        Source      : in  Element_Type;
                        Size        : in  Storage_Count := Element_Type'Size)
      with Pre =>
         Size <= Destination'Size and 
         Size <= Source'Size;

   procedure Byte_Copy (Destination : out Element_Type;
                        Source      : in  Element_Type;
                        Size        : in  Storage_Count := Element_Type'Size)
   is
      subtype Byte_Array is Storage_Array (1 .. Size / System.Storage_Unit);

      Write, Read : Byte_Array;
      for Write'Address use Destination'Address;
      for Read'Address  use Source'Address;
   begin
      Ada.Text_IO.Put_Line("Size to copy =" & Size'Img  &
                           " and Source'Size =" & Source'Size'Img);

      if Size > Destination'Size or else Size > Source'Size then
         raise Constraint_Error with
            "Source'Size < Size or else > Destination'Size";
      end if;

      for N in Byte_Array'Range loop
         Write (N) := Read (N);
      end loop;
   end Byte_Copy;

   procedure Integer_Copy is new Byte_Copy(Integer);
   use type System.Storage_Elements.Storage_Count;

   A, B : Integer;
begin
   A := 5;
   B := 987;
   Ada.Text_IO.Put_Line ("A =" & A'Img);
   Ada.Text_IO.Put_Line ("B =" & B'Img);

   Integer_Copy (A, B, Integer'Size / 2);
   Ada.Text_IO.Put_Line ("A = " & A'Img);
   Ada.Text_IO.Put_Line ("B = " & B'Img);

   Integer_Copy (A, B, Integer'Size * 2);
   Ada.Text_IO.Put_Line ("A =" & A'Img);
   Ada.Text_IO.Put_Line ("B =" & B'Img);
end Test;

如果我理解正确，那么这个程序应该在调用 Put_Line 过程之前引发一些未指定的异常。但是您可以看到，当我运行该程序时，调用该过程时使用了一个无效的 Size 参数，该参数违反了 Precondition Destination'Size ≥ Size ≤ Source'Size。相反，我必须放置一条if语句来实际捕获错误并引发异常 Constraint_Error 以保持正常。

$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A =  987
B =  987
Size to copy = 64 and Source'Size = 32

raised CONSTRAINT_ERROR : Source'Size < Size or else > Destination'Size

我尝试过像添加这样的变体，pragma Precondition ( ... )但这也不起作用。

一件奇怪的事情是，如果我在通用过程主体/定义中重复该with Pre =>子句，程序实际上会编译。它通常不允许过程这样做并引发错误（即，前提条件应该只在正式声明中，而不是在定义中）。在这种情况下，通用过程是一个例外吗？

我也很惊讶 use 子句可以添加到泛型过程声明中。这使得定义形式参数名称更容易（那些非常长的名称），但看起来更像是一个错误，因为这不能用于正常/常规过程声明。

PS 我想用 Ada 语言实现我最接近 C 中的 memcpy() 的模仿，以用于学习目的。

4

1 回答 1

6

您需要通过编译来启用断言-gnata：

$ gnatmake -gnat12 -gnata test.adb
gcc -c -gnat12 -gnata test.adb
gnatbind -x test.ali
gnatlink test.ali
gnatlink: warning: executable name "test" may conflict with shell command

$ ./test
A = 5
B = 987
Size to copy = 16 and Source'Size = 32
A =  987
B =  987

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from test.adb:13 instantiated at test.adb:39

Pragma Assertion_Policy没有在 FSF GNAT <= 4.8 中实现（好吧，你不能用它来打开或关闭检查）。但是，它是在 GNAT GPL 2013 中实现的；如果您不使用 GNAT 项目文件，这意味着创建一个gnat.adc包含

pragma Assertion_Policy (Check);

次要点：'Size以位为单位，而不是字节，所以Storage_Count它真的不是正确的类型！

于 2013-08-28T11:34:28.750 回答