Ada中循环不变量能否依赖参数？程序参数与依赖子句正确性问询

一、参数类型与Depends子句合规性判断 #

参数类型合理性 #

• X和Y声明为in Integer：完全符合逻辑，二者仅作为输入值使用，全程未被修改，是典型的输入参数场景。
• Z声明为out Integer：符合要求，Z作为输出参数，程序中对其进行了明确赋值（初始赋值Z := Y，循环内更新Z := Z - 2），最终输出结果满足后置条件。

Depends子句问题 #

原Depends子句(Z => (Y,Z))不符合程序实际逻辑：

• 从后置条件Z = X - Y和执行流程来看，Z的最终值由X和Y共同决定，完全不依赖自身初始值（Z是out参数，初始值未定义，程序第一行就给Z赋了Y）。
• 正确的Depends子句应为(Z => (X,Y))，准确反映Z的输出仅依赖输入参数X和Y。

二、循环不变量相关疑问解答 #

循环不变量的本质 #

循环不变量属于程序正确性断言，和前置/后置条件作用类似——用于向SPARK验证工具声明循环执行过程中始终保持的逻辑关系，但它嵌入在循环内部，会在每次循环迭代前后被检查。它不属于可执行代码，只是辅助验证的逻辑约束，不会改变参数类型或程序执行流程。

关于in参数X的使用 #

不管是否存在Aux : Integer := X;，在循环不变量中使用X都是合法的：

• X是in参数，全程只读且全局可见，SPARK允许在任何断言（包括循环不变量）中引用它。
• 如果缺失Aux := X;，Aux未初始化，此时循环不变量中引用Aux是非法的（SPARK要求变量使用前必须初始化），但X的引用本身没问题，它依然是in参数，不会因循环不变量的引用改变类型。

关于Z对X的依赖 #

Z的最终值确实依赖X，这是由程序逻辑决定的（通过Aux的初始值关联X，循环中逐步调整Z最终得到X-Y），但这种依赖需要通过Depends子句明确声明，而非由循环不变量决定。循环不变量只是验证Z与X、Aux、Y之间的关系，不会自动修改Depends子句的语义。

附程序代码：

ads文件 #

pragma SPARK MODE;
procedure Myproc (X : in Integer; Y : in Integer; Z : out Integer)
with Depends => (Z => (Y,Z)),
     Post => (Z = X - Y);

adb文件 #

pragma SPARK MODE;
procedure Myproc (X : in Integer; Y : in Integer; Z : out Integer) is
    Aux : Integer := X;
begin
    Z := Y;
    loop
        pragma Loop Invariant (Z = X + Aux - Y);
        exit when Aux = 0;
        Aux := Aux - 1;
        Z := Z - 2;
    end loop;
end Myproc;

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