即使在过程结束时断言相同的条件并且为真，过程上的后置条件也无法证明

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;

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

后置条件可能会失败，无法证明Record_Field_X(Record) = Record_Field_X(Record'Old)

“其他后置条件”在规范和过程结束时的 Assert_And_Cut 之间是相同的。

注意检查更简单的字段，例如 X_Count：

Record_Field_X_Count(记录) = Record_Field_X_Count(记录'旧)

不要引起 gnatprove 的抱怨。

过程中证明者需要做很多工作，因此通常，当证明后置条件出现问题时，有助于在过程结束时断言该条件，以“提醒”证明者这是重要的事实。通常，这是可行的，但在一种情况下，由于某种原因却行不通。

我有什么选择？

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

也许我应该增加运行证明程序的机器上的 RAM，这样它就不会丢失过程结束与其后置条件之间的

Record_Field_X(Record) = Record_Field_X(Record_Old)

事实？ （我目前正在一台具有 32GB 内存的机器上执行此操作，该机器专门用于运行 gnatprove，带有

--memlimit=32000 --prover=cvc4,altergo --steps=0

）

也许还有一些我不知道的技巧？

也许我唯一的选择就是手动校样？

我使用的是spark社区2019版本。

Answer 1

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

--prover=cvc4,altergo,z3 帮助解决问题。