Question

(need in frame -c)
In the given code, Will all the assert statements prove true? Give reason for proved
true or false for each assert statement. [3 M] [CO2]
int main(){
int i = 1;
int x = 33;
/*@
loop invariant 1 <= i <= 19;
loop assigns i;
loop variant 20 - i;
*/
//@assert i == 1;
while(i < 20){
++i;
if(i == 20) break ;
}
//@assert i == 20;
//@assert x == 33;
}

frama-c is a acsl language..

Answer 1

Answer

In the given code all the assert statements will be true.

i. Initially the integer variable 'i' is assigned with 1, and before entering the while loop, the assert statement checks whether 'i' is 1 or not. The variable 'i' will be 1 at this particular statement, hence this assert will prove true.

ii. Inside the while loop the variable 'i' is getting incremented until it reaches 20, when the value of 'i' becomes 20, the control comes out of the while loop. Immediately after the control comes out of the while loop there is a assert statement which checks whether the variable 'i' contains 20 or not. The variable 'i' will be 20 at this particular statement, hence this assert will prove true.

iii. The last assert statement checks whether the value of 'x' is 33 or not. The value of 'x' is initially initialized with 33 and is never modified after that. Hence this assertion will prove true.