--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on February 2014 ---
Hi, I used WP for the following two equivalent behaviours. I started with the first behaviour, WP claimed unknown. behavior STOP_DRUG_MR_Pos: assumes msgId == MSG_CMD_STOP_DRUG; assumes gfMaintenance_Rate > 0; ensures gfPreviousMR == gfMaintenance_Rate; ensures gfMaintenance_Rate == 0; ensures gbDrugTerm == true; I rewrote the above by the following. WP claimed valid. behavior STOP_DRUG_MR_Pos_2: ensures msgId == MSG_CMD_STOP_DRUG && gfMaintenance_Rate > 0 ==> gfPreviousMR == gfMaintenance_Rate && gfMaintenance_Rate == 0 && gbDrugTerm == true; I'm confused why the first one is considered unknown whereas the second one is valid, although both the behaviours are the same. Any comments? Dharma