Постусловие процедуры не подтверждается, даже если в конце процедуры установлено и истинно то же условие.

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

не заставляйте комаров жаловаться.

Внутри процедуры для доказывающего есть довольно много работы, поэтому обычно, когда возникает проблема с доказательством постусловия, он помогает утвердить это условие в конце процедуры, чтобы "напомнить" доказывающему, что это важные факты. Обычно это работает, но в одном случае по какой-то причине нет.

Какие у меня здесь варианты?

Какие могут быть возможные причины этого?

Может, мне просто нужно увеличить оперативную память на машине, на которой я запускаю программу проверки, чтобы она не потеряла Record_Field_X(Record) = Record_Field_X(Record_Old)факт между окончанием процедуры и ее постусловием? (В настоящее время я делаю это на машине с оперативной памятью 32 ГБ, которая используется исключительно для запуска gnatprove, с--memlimit=32000 --prover=cvc4,altergo --steps=0)

Может быть, есть какие-то техники, которых я не знаю?

Может быть, единственный вариант, который у меня есть, - это ручное доказательство?

Я использую версию Spark Community 2019.

Answer 1

Подводя итог комментариям, добавив z3 к пруверам с

--prover=cvc4,altergo,z3

помог решить проблему.