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] Preservation of base loop invariant not verified

>
> Your property P is not provable *by induction* ; it means that P(j+1) is
> not a logic consequence of P(j).


The Concrete Semantics textbook (for which I've only managed to read the
first few chapters) does appear to prefer a induction step of the form:

    loop (Suc n) = Suc n + loop n

but I've tested the solvers with the original property axioms and
assertions of the form:

     ...
     //@ assert loop(8) == 36;
     //@ assert loop(9) == 45;

and the solvers have no problems with them.

By the way, I am aware that this particular problem is best resolved by
testing, but I wanted to find out whether formal verification can prove
that "Hello World!" will be printed using current solvers and a fairly
recent laptop.


(read in the WP manual about the proof obligations generated for loop
> invariants).


Yes I should read the associated manuals from start to finish and study
them carefully, but it's somewhat difficult for me to find the time to do
so since I'm not able to do research all the time.


... It is not proved just because the trivial loop invariant below is
> missing
>


loop invariant j >= 1;


Aha! So the problem was because the solvers did not receive any information
on the lower bound of j. Hmm, okay. Still unclear to me as to why it's
needed, since the invariant doesn't state that j == 1 is false after any
iteration of the loop.


Anyway, I don't see why your loop invariant is splitted into two parts: ...


I intended the first part to be the base case, mirroring what is usually
done when implementing simple recursive algorithms. Now I see that I should
not have done that.


Hope this helps,


Thanks for the help! It would be nice if I could automatically prove the
following loop invariant:

     loop invariant \exists integer k; k >= 1 && k < 10 && (j >= k ==>
is_hello_printed == 1);

but I suppose that could be asking for too much from the solvers.


Best regards,
Khairul


On Mon, Jan 26, 2015 at 7:26 PM, Claude Marche <Claude.Marche at inria.fr>
wrote:

>
> In fact, this does not seem to be the reason. It is not proved just
> because the trivial loop invariant below is missing
>
> loop invariant j >= 1;
>
> with this additional info, the preservation of the loop invariant
>
> loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0);
>
> is a triviality, since j == 1 is false after any iteration of the loop.
>
> Anyway, I don't see why your loop invariant is splitted into two parts:
> this should work :
>
>     /*@ loop invariant j >= 1;
>         loop invariant i == \at(i, LoopEntry) + loop(j - 1);
>         loop invariant j >= 8 ==> is_hello_printed == 1;
>         loop assigns i, j, is_hello_printed;
>         loop variant 10 - j ;
>         */
>
> Hope this helps,
>
> - Claude
>
>
> Le 26/01/2015 10:05, Lo?c Correnson a ?crit :
>
>  Your property P is not provable *by induction* ; it means that P(j+1) is
>> not a logic consequence of P(j).
>> (read in the WP manual about the proof obligations generated for loop
>> invariants).
>> Actually, there is nothing in your loop invariants about the value of (i)
>> at any loop turn?
>> L.
>>
>> _______________________________________________
>> 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
>>
>>
> --
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           |
> Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150127/00f3ecd6/attachment.html>