通过引用或后置条件获取值的 ADA 问题

Question

我对“简单”的 ADA 程序有疑问。本练习旨在通过 ADA 中的参考值和后置条件来学习价值。

在这里，我想构建一个简单的函数，对两个整数求和，其中第一个整数为负数，第二个整数为正数。返回值必须是总和，后置条件必须检查它。 只有当语言集成了正交概念（例如按引用传递和契约）时，这种情况才有可能。

在此代码中：

procedure Tp2q4 is

   function Set_Values(A : in out INTEGER; B : in out INTEGER) return BOOLEAN is
   begin
      A := 2;
      B := 3;
      return TRUE;
   end Set_Values;

   function Sum_Of_Numbers(A, B : in out INTEGER) return INTEGER
     with
       Pre => A < 0 and B > 0,
       Post => (Sum_Of_Numbers'Result = A + B and then Set_Values(A'Access, B'Access))
   is
   begin
      return A + B;
   end Sum_Of_Numbers;

通过此测试：

   A := -1;
   B := 2;
   Put(Sum_Of_Numbers(A,B));
   Put(A);
   Put(B);

我想得到加法、A的修改和B的修改的结果，所以：-1 2 3

但是我得到：-1 1 2

很明显，问题要么是引用值，要么是后置条件......我有什么想法可以解决这个问题吗？

Answer 1

您没有给出实际的编译示例，所以我检查了，我能看到的最好的结果是您没有打开断言来启用后置条件。请注意，根据您发布的代码，结果应该是 1 2 3，而不是 -1 2 3。我尝试解释您的实际代码是什么，并且以下示例有效（尽管我根本不建议使用这样的后置条件.这是一个非常糟糕的主意......你需要重新考虑你的设计）。

with Ada.Text_IO; use Ada.Text_IO;

procedure jdoodle is

    pragma Assertion_Policy(Check);

    function Set_Values(A : in out INTEGER; B : in out INTEGER) return BOOLEAN is
    begin
      A := 2;
      B := 3;
      return TRUE;
    end Set_Values;
    
    function Sum_Of_Numbers(A, B : in out INTEGER) return INTEGER
     with
       Pre => A < 0 and B > 0,
       Post => (Sum_Of_Numbers'Result = A + B and then Set_Values(A, B))
    is
    begin
      return A + B;
    end Sum_Of_Numbers;
    
    A, B : Integer;
begin
    A := -1;
    B := 2;
    Put_Line(Sum_Of_Numbers(A,B)'Image);
    Put_Line(A'Image);
    Put_Line(B'Image);
end jdoodle;

Result:
 1
 2
 3

gcc -c jdoodle.adb
gnatbind -x jdoodle.ali
gnatlin

k jdoodle.ali -o jdoodle