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

  • Subject: [Frama-c-discuss] Preservation of base loop invariant not verified
  • From: kazarmy at gmail.com (Khairul Azhar Kasmiran)
  • Date: Sun, 25 Jan 2015 13:36:27 +0800
  • In-reply-to: <CA+Tazt7sOtQxyvgLwbFvWDQ=pniO2AQFh-xC216vEXd9aOprqQ@mail.gmail.com>
  • References: <CA+Tazt7sOtQxyvgLwbFvWDQ=pniO2AQFh-xC216vEXd9aOprqQ@mail.gmail.com>
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>