Ada程序按引用传值与后置条件问题求助

问题根源 #

1. 后置条件的误用：Ada的契约（前置/后置条件）仅用于验证约束，不能用来执行带副作用的操作（比如修改输入参数）。你在Sum_Of_Numbers的后置条件里调用Set_Values修改A、B，属于违背契约设计规范的行为，会导致未定义的参数状态。
2. 参数逻辑顺序错误：你试图通过后置条件修改参数，但函数体内未处理参数修改逻辑，导致实际执行时参数的修改时机和取值不符合预期。

修正方案 #

将参数修改逻辑从后置条件移到函数体内，同时用契约的Old属性验证返回值与初始参数的关系，确保逻辑清晰且符合Ada规范。

修正后的完整代码

procedure Tp2q4 is
   with Ada.Text_IO; use Ada.Text_IO;

   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 = Sum_Of_Numbers'Old(A) + Sum_Of_Numbers'Old(B))
               and then A = 2 and B = 3
   is
      Temp_Sum : INTEGER;
   begin
      Temp_Sum := A + B; -- 先计算初始两数之和
      Set_Values(A, B);  -- 在这里执行参数修改逻辑
      return Temp_Sum;
   end Sum_Of_Numbers;

   A, B : INTEGER;
begin
   A := -1;
   B := 2;
   Put(Sum_Of_Numbers(A, B)'Image & " ");
   Put(A'Image & " ");
   Put(B'Image);
   New_Line;
end Tp2q4;

关键说明 #

• 使用Sum_Of_Numbers'Old(A)获取函数执行前的参数值，确保后置条件能准确验证返回值与初始输入的关系。
• 将Set_Values的调用移到函数体内，先计算求和结果再修改参数，保证逻辑顺序符合预期。
• 后置条件仅保留验证逻辑：确认返回值正确，且参数已被修改为目标值。

测试输出 #

运行代码后会得到： 1 2 3（Ada的Image属性会为整数添加前导空格，若需要无空格输出，可使用Put(Integer'Image(X)(2..Integer'Image(X)'Length))），与你的预期一致。

内容的提问来源于stack exchange，提问作者Simon Riou