--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2014 ---
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