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] Some unproved VCs occur while using wp

  • Subject: [Frama-c-discuss] Some unproved VCs occur while using wp
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Thu, 10 May 2012 16:37:50 +0200
  • In-reply-to: <CAC3Lx=bS+FJFz86+mPagZL90Vf5BSrHKEGNbwhfsHmYxPMF-2Q@mail.gmail.com>
  • References: <E1SR979-0000Fg-4F.naveugene-mail-ru@f159.mail.ru> <CAC3Lx=bS+FJFz86+mPagZL90Vf5BSrHKEGNbwhfsHmYxPMF-2Q@mail.gmail.com>
Hello David,

2012/5/9 David MENTRE <dmentre at linux-france.org>:
>
> Goal store_cisapb_post_1 cannot be proved. You probably meant "ensures
> Equal{Post}(a, b, c, n);", i.e. equality on Post state. Equality in
> Pre state is obviously invalid. With this modification this VC is
> proved.
>
> For store_cisapb_loop_inv_2_preserved goal, I have used a slightly
> different loop invariant:
> """
> loop invariant \forall integer k; 0 <= k < i ==> c[k] == a[k] + b[k];
> """
>
> For store_cisapb_assert_6_rte goal, I used the same assumption as you,
> only limiting the assumption to 0 <= k < n.
>

For what it's worth, strictly speaking, it is not necessary to unfold
the definition Equal in the loop invariant: I didn't succeed to have
it discharged automatically, but you can convince Coq that it is true
(I don't append the script here, especially given the fact that I'm
using the development version of Frama-C, but if someone is
interested, feel free to ask). My guess is that automated provers have
trouble relating the Equal predicate of the previous loop step (given
as hypothesis) and the Equal of the current step (the goal of the
proof obligation), but this might require further investigation.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile