Question

Verify that the program segment

if x < 0 then x : = 0

is correct with respect to the initial assertion T and the final assertion.

Short answer

Thus, it is verified with start and end assertion.

Step-by-step solution

Program Segment

Suppose that program S is divided into subprograms ${\mathrm{S}}_1$and ${\mathrm{S}}_2$, denote by

$S={\mathrm{S}}_1:{\mathrm{S}}_2$

Assume the correctness of${\mathrm{S}}_1$ with respect to the initial statement p and the final statement q, the correctness of${\mathrm{S}}_2$ with respect to the initial statement p, and the final statement r.

A rule of inference called a compositional rule that can be stated as

$\begin{array}{c}\mathrm{p}\left\{{\mathrm{S}}_1\right\}\mathrm{q}\\ \frac{\mathrm{q}\left\{{\mathrm{S}}_2\right\}r}{\therefore \mathrm{p}\left\{{\mathrm{S}}_1,{\mathrm{S}}_2\right\}r}\end{array}$

Given

Given in the question, we need to verify the program segment,

If x < 0 then x : = 0 and the final assertion x > 0 .

Solution

Here we solve our question,

x > 0then x : 0

When the initial statement is true and x > 0 , then the assignment x = 0 is made.

The last statement asserting that x > 0 is true in this case.

Additionally, when the initial statement is true and is false. Therefore x > 0 the final statement is again true.

Here we use inference of program segment rule, the segment is valid with respect to the given start and end assertion.

Hence, it is verified with start and end assertion.