--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Preservation of base loop invariant not verified



Dear all,

Since tabs apparently do not survive the mailing list process, I provide
the same code below (also attached) but with spaces instead of tabs:

#include <stdio.h>

/*@ axiomatic loop28 {
        logic integer loop(integer k);
        axiom loop_base:
           loop(0) == 0;
        axiom loop_inductive:
           \forall integer k; k > 0 ==> loop(k) == k + loop(k - 1);
    }
 */

int main(void) {
    int i = 0;
    int j;
    //@ ghost int is_hello_printed = 0;

    /*@ loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0);
        loop invariant j >= 2 ==> i == \at(i, LoopEntry) + loop(j - 1);
        loop invariant j >= 8 ==> is_hello_printed == 1;
        loop assigns i, j, is_hello_printed; */
    for (j = 1; j < 10; j++) {
        i += j;
        if (i == 28) {
            puts("Hello World!");
            //@ ghost is_hello_printed = 1;
        }
    }

    //@ assert is_hello_printed == 1;
}

Best regards,
Khairul


On Sun, Jan 25, 2015 at 1:24 PM, Khairul Azhar Kasmiran <kazarmy at gmail.com>
wrote:

> Dear all,
>
> I'm trying to verify the following code with Frama-C and WP:
>
> #include <stdio.h>
>
> /*@ axiomatic loop28 {
>         logic integer loop(integer k);
>         axiom loop_base:
>            loop(0) == 0;
>         axiom loop_inductive:
>            \forall integer k; k > 0 ==> loop(k) == k + loop(k - 1);
>     }
>  */
>
> int main(void) {
> int i = 0;
> int j;
> //@ ghost int is_hello_printed = 0;
>
> /*@ loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0);
>     loop invariant j >= 2 ==> i == \at(i, LoopEntry) + loop(j - 1);
>     loop invariant j >= 8 ==> is_hello_printed == 1;
>     loop assigns i, j, is_hello_printed; */
> for (j = 1; j < 10; j++) {
> i += j;
> if (i == 28) {
> puts("Hello World!");
> //@ ghost is_hello_printed = 1;
> }
> }
>
> //@ assert is_hello_printed == 1;
> }
>
> Currently, all generated VCs are verified except the preservation of the
> first loop invariant (i.e. the invariant with j==1).This is what Frama-C
> generates for it:
>
> Goal Preservation of Invariant (file loop28_induct.c, line 17):
> Assume { (* Domain *) Type: (is_sint32 i_3). }
> Prove: i_3=(L_loop 0).
>
> which is obviously unprovable, but does suggest that the problem can be
> fixed if an equation for i_3 can be provided. Indeed, if I add the
> following loop invariant before all the other invariants:
>
> loop invariant i == \at(i, LoopEntry) + ((j - 1) * j) / 2;
>
> everything is verified, including all of the original invariants in the
> code above. However, I don't want to do this, primarily because such
> equations may not be available for other problems similar to this one.
>
> My questions:
>   1. Why can't Frama-C verify the first loop invariant's preservation?
>   2. What can I do to fix this, without involving the loop equation for i
> stated above?
>
> I'm using Frama-C (Neon) with Alt-Ergo 0.99.1 and Z3 4.3.2.
>
> Best regards,
> Khairul
>
>
>
>
> --
> Dr. Khairul Azhar Kasmiran
> Room C3-14, Department of Computer Science,
> Faculty of Computer Science and Information Technology,
> Universiti Putra Malaysia,
> 43400 UPM Serdang, Selangor,
> Malaysia.
> Tel: +603 8947 1657
> Fax: +603 8946 6576
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150125/102cf4e5/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: loop28_induct.c
Type: text/x-csrc
Size: 805 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150125/102cf4e5/attachment-0001.c>