Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.

Le vendredi 05 juin 2009 ? 17:36 +0200, Nicolas Stouls a ?crit :

> The conversion Integer -> int is not costless for automatic provers. The "exact" 
> option removes conversion predicates. It is then more efficient. However, is 
> there any sense to prove a program without these conversions ?
> 
> In my opinion, there is really 2 disjoint goals :
>     * is my program correct without machine constraints ? (abstract Integers)
>         --> exact option
> 
>     * are abstract values equals to concrete ones in previous PO ?
>         --> if yes : just smile
>             if not : same player play again, but without exact option.
> 
> I don't know how to verify this second point. But I think that if a PO is valid 
> with Integers and timeout without, then a manual proof can be tried.

The "bounded" integer model (or "strict" depending on the stage) fits
these two goals quite well. Jessie generates a first set of POs for
program correctness. These POs are using mathematical integers, hence
are prover-friendly, presumably. But it also generates a second set of
POs. These other POs ensure that the abstract values are equal to the
concrete values, by stating that the computations do not overflow.

Therefore, if a program is proved correct with respect to the "bounded"
model, it is also correct in real life. (This property is not true for
the "exact" model.) But some correct real-life programs may falsify some
POs of the "bounded" model. These specific programs need the "modulo"
model, but they are hopefully uncommon and most programs can be proved
correct with the "bounded" model.

In your previous mail, you give a short explanation of the "bounded"
model; but it may lead to some confusion depending on the background of
the reader. (Had I not known what it meant beforehand, I would have
gotten it wrong from your sentence.) So, for the record, let me just
stress than the "bounded" model does not describe a saturating
arithmetic, it describes a modulo integer arithmetic (or saturating or
trapping or whatever 2-complement arithmetic you can imagine) with
additional POs proving that the values do not overflow.

Best regards,

Guillaume