--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Checking for side-effects



Isn't this what the 'assigns' clause is for?
As in

/*@
     requires global == dummy;

     behavior GLOBAL_BELOW_5:
       assumes global < 5;
       assigns global;
       ensures global == \old(global) + 1;
    
     behavior GLOBAL_ABOVE_5:
       assumes global > 5;
       assigns global;
       ensures global == \old(global) - 1;

     behavior GLOBAL_EQUAL_5:
       assumes global == 5;
       assigns \nothing;
  
     complete behaviors;
     disjoint behaviors;
*/

- David

On 2/6/2014 2:47 PM, Dharmalingam Ganesan wrote:
> Hi,
>
> Is there a way to specific "negative" behaviours, for example, no variable should be updated except the given variable.
>
> For example, for this little code, WP can able to prove all behaviours. That's great. But, I do not want any change in the state of the system except the "global" value. In this code, the dummy variable's state can also change, which is an undesirable side-effect (let's assume).
>
> For large and complex code, it appears specifying what is not allowed would also help to make sure implementation = specification.
>
> I looked into -deps option to Frama-c, it appears to list the dependencies for each variable, which is helpful, but it does not quite check for undesired state changes.
>
> Any comments?
> Dharma
>
>
> int global = 0;
> int dummy = 0;
>
> /*@
>      requires global == dummy;
>
>      behavior GLOBAL_BELOW_5:
>        assumes global < 5;
>        ensures global == \old(global) + 1;
>     
>      behavior GLOBAL_ABOVE_5:
>        assumes global > 5;
>        ensures global == \old(global) - 1;
>
>      behavior GLOBAL_EQUAL_5:
>        assumes global == 5;
>        assigns \nothing;
>   
>      complete behaviors;
>      disjoint behaviors;
> */
> void update()
> {
>     if(global < 5) {
>         global++;
>         dummy++;
>     }
>
>     if(global > 5) {
>         global--;
>         dummy--;
>     }
> }
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss