--- layout: fc_discuss_archives title: Message 125 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



Hello,

I encounter some difficulties with predicates and logic functions.
Here is two very small exemples.
The first one is made with logic functions whereas the other one is made
with predicates.
  * in the first one, I cannot prove the posts
  * in the second, the first post is proved, but the second post is
commented (syntax error)
Can you see my problems ?

thanks in advance,

St?phane


/*@ logic boolean cond1(integer p) = (p>0)?\true:\false ;
  @ logic boolean cond2(integer p) = (p<10)?\true:\false ;
  @ logic boolean cond3(boolean c1, boolean c2) = c1 && c2 ;
  @*/

/*@ 
  @ ensures (cond1(x) && cond2(y)) ==> \result == 1 ;
  @ ensures \result == ((cond3(cond1(x),cond2(y)))?1:0);
  @*/
int ftest(int x, int y)
{
  return (x>0 && y<10);
}

/*@ predicate pcond1(integer p) = (p>0)?\true:\false ;
  @ predicate pcond2(integer p) = (p<10)?\true:\false ;
  @ predicate pcond3(boolean c1, boolean c2) = c1 && c2 ;
  @*/

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