Question

Devise a rule of inference for verification of partial correctness of statements of the form

$$\begin{gathered} \mathbf{if}\mathbf{}\mathbf{condition}\mathbf{}\mathbf{1}\mathbf{}\mathbf{then} \\ {\mathbf{S}}_{\mathbf{1}} \\ \mathbf{else}\mathbf{}\mathbf{if}\mathbf{}\mathbf{condition}\mathbf{}\mathbf{2}\mathbf{}\mathbf{then} \\ {\mathbf{S}}_{\mathbf{2}} \\ \mathbf{⋮} \\ \mathbf{else} \\ {\mathbf{S}}_{\mathbf{n}} \\ \mathbf{where}\mathbf{}{\mathbf{S}}_{\mathbf{1}}\mathbf{,}{\mathbf{S}}_{\mathbf{2}}\mathbf{,}\mathbf{.}\mathbf{.}\mathbf{.}\mathbf{.}\mathbf{.}\mathbf{.}\mathbf{.}\mathbf{,}{\mathbf{S}}_{\mathbf{n}}\mathbf{}\mathbf{are}\mathbf{}\mathbf{blocks} \end{gathered}$$

Short answer

Thus$\frac{(\mathrm{P}\wedge \mathrm{\neg }(\text{condition}1)\wedge \mathrm{\neg }(\text{conditon2}2)\dots \dots \dots \wedge \mathrm{\neg }(\text{condition}\mathrm{n}-1\left)\right)\left\{{\mathrm{S}}_{\mathrm{n}}\right\}\mathrm{q}}{\left.\therefore \mathrm{P}\text{if condition}1\text{then}{\mathrm{S}}_1\text{if condition}2\text{then}{\mathrm{S}}_2\dots \dots ..\text{else}{\mathrm{S}}_{\mathrm{n}}\right\}\mathrm{q}}\text{.}$

Step-by-step solution

Inference of the program segment rule.

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,

$$\begin{gathered} \mathrm{if}\mathrm{condition}1\mathrm{then} \\ {\mathrm{S}}_1 \\ \mathrm{else}\mathrm{if}\mathrm{condition}2\mathrm{then} \\ {\mathrm{S}}_2 \\ ⋮ \\ \mathrm{else} \\ {\mathrm{S}}_{\mathrm{n}} \\ \mathrm{where}{\mathrm{S}}_1,{\mathrm{S}}_2,.......,{\mathrm{S}}_{\mathrm{n}}\mathrm{are}\mathrm{blocks} \end{gathered}$$

Solution

We know here we solve our question, let P be the initial assertion.

Let q be the final assertion, if the condition is true then$S_1$will get executed.

So,

$\left(P\wedge \text{condition1)}\left\{S_1\right\}q\right.$

If condition 2 is true and condition 1 is false.

Then$S_2$will be executed.

So, $(P\wedge \mathrm{\neg }(\text{condition}1)\wedge (\text{conditon}2\left)\right)\left\{S_1\right\}q$.

Similarly,

$(\mathrm{P}\wedge \mathrm{\neg }(\mathrm{condition})\wedge \mathrm{\neg }(\mathrm{condition})........\wedge (\mathrm{condition}\mathrm{n}-1\left)\right)\left\{{\mathrm{S}}_{\mathrm{n}}\right\}\mathrm{q}$

entire statement.

So,

$\begin{array}{r}(\mathrm{P}\wedge \text{condition}1)\left\{{\mathrm{S}}_1\right\}\mathrm{q}\\ (\mathrm{P}\wedge \mathrm{\neg }(\text{condition}1)\wedge (\text{conditon}2\left)\right)\left\{{\mathrm{S}}_1\right\}\mathrm{q}\\ ⋮\\ \frac{(\mathrm{P}\wedge \mathrm{\neg }(\text{condition}1)\wedge \mathrm{\neg }(\text{conditon}2)\dots \dots \dots \wedge \mathrm{\neg }(\text{condition}\mathrm{n}-1\left)\right)\left\{{\mathrm{S}}_{\mathrm{n}}\right\}\mathrm{q}}{\therefore \mathrm{P}\left\{\text{if condition}1\text{then}{\mathrm{S}}_1\text{if condition}2\text{then}{\mathrm{S}}_2\dots \dots ..\text{else}{\mathrm{S}}_{\mathrm{n}}\right\}\mathrm{q}}.\end{array}$

Hence,$\frac{(P\wedge \mathrm{\neg }(\text{condition1})\wedge \mathrm{\neg }(\text{conditon}2)\dots \dots \dots \wedge \mathrm{\neg }(\text{condition}n-1\left)\right)\left\{S_n\right\}q}{\therefore P\left\{\text{if condition}1\text{then}{S}_1\text{if condition}2\text{then}{S}_2\dots \dots .\text{else}{S}_n\right\}q}$