时间戳

首页 > 解决方案 > 即使在程序结束时断言了相同的条件并且为真，程序上的后置条件也不能证明

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

问题描述

代码如下所示：

规格：

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) = Record_Field_X_Count(Record'Old)

不要让 gnatprove 抱怨。

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

我在这里有什么选择？

这可能是什么原因？

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

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

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

我正在使用 spark 社区 2019 版。

标签： adaspark-adaspark-2014

解决方案

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

--prover=cvc4,altergo,z3

帮助解决了这个问题。

推荐阅读