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] "\at(var, Pre)" before a loop

Just for fun, I will say:

/*@
loop invariant 0<=i<100;
loop invariant \at(t[i], Pre) == 1 && t[i] == \at(t[i], Pre) + 1;
*/
for (i=0; i<100; i++) t[i]++;

Do I win something??? :)
--
Thomas P.

-----Message d'origine-----
De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de CUOQ Pascal
Envoy? : jeudi 2 avril 2009 20:38
? : Frama-C public discussion; frama-c-discuss at lists.gforge.inria.fr
Objet : Re: [Frama-c-discuss] "\at(var, Pre)" before a loop


>> In other words, is this loop invariant correct? 
>
>\at(expr,Pre) always denotes the value of expr in the pre-state of the
>function (i.e. when the function is entered). Assuming there's no
>overflow or invalid pointer access, the loop invariant is correct.

On the subject of the two caveats expressed by Virgile,
I would like to add this:

1/ when you subtract two valid pointers with the same base address,
the result is never an overflow, so do not worry about that and
worry about the validity instead.

2/ Your function presumably has a precondition that looks like
"\valid_range(pString, 0, nbBytes)" (perhaps +/-1, I never know).
If I was you and if I wasn't able to prove the correctness of
my function, one of the things I would try first would be to
replicate that precondition inside the invariant:

loop invariant i == pString - \at(pString, Pre) && 
       \valid_range(\at(pString, Pre), 0, nbBytes) ;

As Virgile explained in another thread, loops are very much treated
as opaque blocks by those analyzers that are based on Hoare logic.
If you need a property after or even inside the loop,
you usually need to put it in the loop invariant,
even if it's orthogonal to what the loop does (and it's very easy to
forget in this case).

Actually it's so annoying that most analyzers try to save you the writing
of these parts of the invariant, hence my reserves. It may not be
necessary with Jessie. But it doesn't hurt to try.

Here's a fun little exercice on the same topic : 
if you have the property that every cell in an int array t[100]
contains 1, what is the invariant for proving that every cell contains 2
after executing the following loop:
for (i=0; i<100; i++) t[i]++;

Pascal
PS: solution in my next post.


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

Ce courriel (incluant ses eventuelles pieces jointes) peut contenir des informations confidentielles et/ou protegees ou dont la diffusion est restreinte. Si vous avez recu ce courriel par erreur, vous ne devez ni le copier, ni l'utiliser, ni en divulguer le contenu a quiconque. Merci d'en avertir immediatement l'expediteur et d'effacer ce courriel de votre systeme. Astrium decline toute responsabilite en cas de corruption par virus, d'alteration ou de falsification de ce courriel lors de sa transmission par voie electronique.
This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient, please notify the sender immediately, do not copy this message or any attachments and do not use it for any purpose or disclose its content to any person, but delete this message and any attachments from your system. Astrium disclaims any and all liability if this email transmission was virus corrupted, altered or falsified. 
---------------------------------------------------------------------
Astrium SAS (393 341 516 RCS Paris) - Siege social: 6 rue Laurent Pichat, 75016 Paris, France