Le code ressemble à ceci:

Spec:

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;

Corps:

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;

Il n'y a pas d'erreurs de preuve dans le corps, l'erreur est uniquement sur la spécification :

la postcondition peut échouer, ne peut pas prouver Record_Field_X(Record) = Record_Field_X(Record'Old)

Les 'autres postconditions' sont identiques entre la spécification et l'Assert_And_Cut à la fin de la procédure.

Notez les vérifications avec des champs plus simples, comme X_Count :

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

Ne faites pas se plaindre gnatprove.

Il y a beaucoup de travail pour le prouveur à l'intérieur de la procédure, donc généralement, lorsqu'il y a un problème pour prouver la postcondition, il est utile d'affirmer cette condition à la fin de la procédure pour "rappeler" au prouveur qu'il s'agit de faits importants. Habituellement, cela fonctionne, mais dans un cas, cela ne fonctionne pas pour une raison quelconque.

Quelles sont mes options ici?

Quelles peuvent être les causes possibles de cela ?

Peut-être devrais-je simplement augmenter la RAM sur la machine sur laquelle j'exécute le test, afin qu'il ne perde pas le fait Record_Field_X(Record) = Record_Field_X(Record_Old) entre la fin de la procédure et sa postcondition ? (Je fais actuellement cela sur une machine avec 32 Go de RAM qui est utilisée exclusivement pour exécuter gnatprove, avec --memlimit=32000 --prover=cvc4,altergo --steps=0)

Peut-être y a-t-il des techniques que je ne connais pas ?

Peut-être que la seule option que j'ai est la preuve manuelle ?

J'utilise la version 2019 de la communauté Spark.

4
Dmitry Petukhov 18 févr. 2020 à 11:25

1 réponse

Meilleure réponse

Pour résumer les commentaires, en ajoutant z3 aux prouveurs avec

--prover=cvc4,altergo,z3

Aidé à résoudre le problème.

5
jklmnn 19 févr. 2020 à 10:08