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] logic function and predicates

Hi,

Your problems come from the fact booleans terms and propositions are not the
same, and provers do not treat them identically.

  * in the first one, I cannot prove the posts


In this case, you attempt to treat everything as boolean terms, which is not
the best thing to do with automatic provers. As a result, only Alt-Ergo
manages to prove all the VC, while Simplify, Z3 and Yices fail on some.
Maybe Jean-Christophe will have an idea why it is the case, maybe some
problem with the encoding to SMT format?


>
>  * in the second, the first post is proved, but the second post is
> commented (syntax error)


when you write

@ //ensures \result == ((pcond3(pcond1(x),pcond2(y)))?1:0);

you assume that pcond1, pcond2 and pcond3 are logic functions that return a
boolean. This is not the case. In your example, these are predicates, whose
application is a proposition that cannot be used inside terms. Please refer
to the grammar of terms and propositions in ACSL reference (section 2.2),
you will see a proposition cannnot occur as an argument of an application,
and it can occur inside a proposition (a?b:c) only when b and c are
themselves propositions. If you rewrite your example this way, all VC are
proved by all the provers I mentioned:

/*@ predicate pcond1(integer p) = (p>0)?\true:\false ;
 @ predicate pcond2(integer p) = (p<10)?\true:\false ;
 @*/

/*@
 @ ensures (pcond1(x) && pcond2(y)) ==> \result == 1 ;
 @ ensures \result == 1 <==> pcond1(x) && pcond2(y);
 @*/
int ftest2(int x, int y)
{
 return (x>0 && y<10);
}

Then, you may want to express this property with behaviors, in the following
way:

/*@ predicate pcond1(integer p) = p > 0;
  @ predicate pcond2(integer p) = p < 10;
  @*/

/*@ behavior ok:
  @   assumes pcond1(x) && pcond2(y);
  @   ensures \result == 1;
  @ behavior ko:
  @   assumes !pcond1(x) || !pcond2(y);
  @   ensures \result == 0;
  @*/
int ftest2(int x, int y)
{
 return (x>0 && y<10);
}

HTH,
--
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081031/7aa7761e/attachment.html