即使相同的条件在程序结束时被断言并为真，程序的后置条件也不能证明

Question

代码如下所示：

规格：

type Some_Record_Type is private;

procedure Deserialize_Record_Y(Record: in out Some_Record_Type)
with Post => (
    if Status_OK then (
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record'Old)
    )
);

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type;
function Record_Field_X_Count(Record: Some_Record_Type) return Natural;

正文：

type Some_Record_Type is
   record
      X_Count: Natural;
      X      : X_Bounded_Array_Type;
      Y_Count: Natural;
      Y      : Y_Bounded_Array_Type;
      ...
   end record;

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type
is (
   ...
   a bit of logic based on values of other fields of Record
   ...
)

function Record_Field_X_Count(Record: Some_Record_Type) return Natural
is (Record.X_Count);

procedure Deserialize_Record_Y(Record: in out Some_Record_Type) is
    Old_Record: Some_Record_Type := Record with Ghost;
begin
    ...
    -- updates the Y field of the Record.
    -- Note that we annot pass Record.Y and have to pass
    -- the whole Record because Record is a private type
    -- and Deserialize_Record_Y is in public spec
    ...
    pragma Assert_And_Cut (
        Status_OK
        and then
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record_Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record_Old)
    )
end Deserialize_Record_Y;

正文中没有证明错误，错误仅在规范上：

postcondition might fail, cannot prove Record_Field_X(Record) = Record_Field_X(Record'Old)

'other postconditions' 与程序结束时的规范和 Assert_And_Cut 相同。

请注意具有更简单字段的检查，例如 X_Count:

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

不要让 gnatprove 抱怨。

过程中的证明者需要做很多工作，所以通常，当证明后置条件有问题时，它有助于在过程结束时向 'remind' 证明者断言该条件是重要的事实。通常，这是有效的，但在一种情况下，由于某种原因它不起作用。

这里我有哪些选择？

这可能是什么原因造成的？

也许我应该增加运行验证器所在机器上的 RAM，这样它就不会丢失过程结束与其后置条件之间的 Record_Field_X(Record) = Record_Field_X(Record_Old) 事实？（我目前正在一台配备 32GB 内存的机器上执行此操作，该机器专门用于运行 gnatprove，使用 --memlimit=32000 --prover=cvc4,altergo --steps=0）

可能有些技巧我不知道？

也许我唯一的选择是手动证明？

我用的是spark community 2019版。

Answer 1

为了总结评论，将 z3 添加到证明者中

--prover=cvc4,altergo,z3

帮助解决了问题。

即使相同的条件在程序结束时被断言并为真，程序的后置条件也不能证明

Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure

ada

spark-ada

spark-2014