Question

Hello, would like help with the following question please:

2 This question is on formal methods and software verification (i) Explain why a formal specification of a program is more effective if it is considerably shorter than the program that implements the [6 marks] specification (ii) Given the following program x = 0; while (m !- 9) x x + 100; here m and x are integer variables (a) Identify the program input variable or variables (b) Identify the program output variable or variables (c) Give the pre-condition on the input that ensures that the program (d) Give the pre-condition on the input that ensures the program post- [2 marks] [2 marks] terminates 5 markS] [5 marks] condition x 1002

Answer 1

1. By means of formal specification, a combat (precise form) form of the model is possible. So easily specified in the modularized form where it is feasible to prove that a code snippet relies on its specifications. The main advantage of using a formal method is it can minimize the amount of faults in the system. It is also cost-effective when comparing with a program that implements the specification

2. In the below mentioned code snippet, there are 2 variables.

x=0;

while (m!=9)

{

m=m-1;

x=x+100;

}

The two variables are x and m.

The code snippet says that “While m not equal to 9, reduce the value of m by 1 and then increment x by 100. When you get to 9, exit the while statement and go out of the loop.

It is given that x and m are integers.

Program input variable is m, where user gives value for executing the while loop condition.

Program output variables are m and x, where after execution value of m and x can be accessed.

If the condition is false, while loop is terminated. So it will be m==9

Value of x will go like x=0, x=100, x=200, x=300……..x=1000, x=1100…. based on input value m. To make it <1002, loop should terminate when x becomes 1000 or less than 1000. That is maximum 10 iterations. If m==20, In first iteration it becomes m-1=19, then 18,17….etc as each iteration proceeds.

So the condition is m==20.