我对“简单”的 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
很明显,问题要么是引用值,要么是后置条件......我有什么想法可以解决这个问题吗?
您没有给出实际的编译示例,所以我检查了,我能看到的最好的结果是您没有打开断言来启用后置条件。请注意,根据您发布的代码,结果应该是 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