--- layout: fc_discuss_archives title: Message 126 from Frama-C-discuss on October 2008 ---
[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