--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using a identifier in an "assumes" clause



Hello,

Your problem comes from a lack of alt-ergo.
As you can see in this example, the goal ok and ko are equivalent.
Alt-ergo 0.94 can only prove the first one :
 > cat test.why
goal ko:
   forall b_0:int. forall a_0:int.
   (let diff_0 = (a_0-b_0) in (0 <= diff_0))
   -> ((a_0 < b_0) -> (b_0 = a_0))
goal ko:
   forall b_0:int. forall a_0:int.
   (forall diff_0:int. (diff_0 = (a_0-b_0)) -> (0 <= diff_0))
   -> ((a_0 < b_0) -> (b_0 = a_0))
 >alt-ergo test.why
Inconsistent assumption
File "test.why", line 1, characters 1-150:File "test.why", line 1, 
characters 1-150:Valid (0.0100) (2)
File "test.why", line 5, characters 1-176:I don't know

Now, WP plugin translates \let constructs of ACSL into forall and 
equalities constructs of Alt-ergo in order to work around a bug of 
alt-ergo 0.93.
The option "-wp-norm Let" can be used to keep let constructs into goals 
for alt-ergo.
With this option, your two goals can be verified.

When subtitution does not give too big goals, you can also use the 
option  "-wp-norm Exp"

 > frama-c -wp-help
...
-wp-norm <norm>     Predicate normalization for Coq and Alt-Ergo provers:
                     - Eqs: replace let-bindings by equalities (default).
                     - Let: preserve let-bindings.
                     - Exp: let-expansion.
                     - Cc:  generates local functions by closure-conversion
...

Patrick.



02/03/2012 17:30, mohamed belasri wrote:
> Hi,
>
> I tried to verify the following example by using an identifier (diff) to
> simplify the assumption :
> /*@
>    @ behavior b1:
>    @     assumes      \let diff=(a-b);         diff>=0;
>    @     ensures \result==a;
>    @ behavior b2:
>    @     assumes      \let diff=(a-b);        diff<0;
>    @     ensures \result==b;
>    @ complete behaviors;
>    @ disjoint behaviors;
>    @*/
>
> int max(int a, int b){
>      if(a>=b)
>          return a;
>      else
>          return b;
> }
>
> but I realized that the WP plug-in couldn't verify that the assumption
> "diff>=0" is equivalent to "a>=b", so he could not verify for example that
> \result==a.
> However, we can easily verify the same function if don't use an identifier :
> /*@
>    @ behavior b1:
>    @     assumes     (a-b)>=0;
>    @     ensures \result==a;
>    @ behavior b2:
>    @     assumes    (a-b)<0;
>    @     ensures \result==b;
>    @ complete behaviors;
>    @ disjoint behaviors;
>    @*/
>
> So, if anyone know why we have such a problem ...
>
> Regards.
>