The design approach used in cleanroom software engineering makes heavy use of the structured programming philosophy. But in this case, stru...

The design approach used in cleanroom software engineering makes heavy use of the structured programming philosophy. But in this case, structured programming is applied far more rigorously.

Basic processing functions (described during earlier refinements of the specification) are refined using a “stepwise expansion of mathematical functions into structures of logical connectives [e.g., if-then-else] and subfunctions, where the expansion [is] carried out until all identified subfunctions could be directly stated in the programming language used for implementation”.

Basic processing functions (described during earlier refinements of the specification) are refined using a “stepwise expansion of mathematical functions into structures of logical connectives [e.g., if-then-else] and subfunctions, where the expansion [is] carried out until all identified subfunctions could be directly stated in the programming language used for implementation”.

The structured programming approach can be used effectively to refine function, but what about data design? Here a number of fundamental design concepts come into play. Program data are encapsulated as a set of abstractions that are serviced by subfunctions. The concepts of data encapsulation, information hiding, and data typing are used to create the data design.

**Design Refinement and Verification**

Each clear-box specification represents the design of a procedure (subfunction) required to accomplish a state box transition. With the clear box, the structured programming constructs and stepwise refinement are used as illustrated in figure. A program function, f, is refined into a sequence of subfunctions g and h. These in turn are refined into conditional constructs (if-then-else and do-while). Further refinement illustrates continuing logical refinement.

At each level of refinement, the cleanroom team performs a formal correctness verification. To accomplish this, a set of generic correctness conditions are attached to the structured programming constructs. If a function f is expanded into a sequence g and h, the correctness condition for all input to f is

**• Does g followed by h do f ?**

When a function p is refined into a conditional of the form, if c then q, else r, the correctness condition for all input to p is

**• Whenever condition c is true, does q do p; and whenever c is false, does r do p?**

**When function m is refined as a loop, the correctness conditions for all input to m are**

**• Is termination guaranteed?**

• Whenever c is true, does n followed by m do m; and whenever c is false, does skipping the loop still do m?

• Whenever c is true, does n followed by m do m; and whenever c is false, does skipping the loop still do m?

Each time a clear box is refined to the next level of detail, these correctness conditions are applied.

It is important to note that the use of the structured programming constructs constrains the number of correctness tests that must be conducted. A single condition is checked for sequences; two conditions are tested for if-then-else, and three conditions are verified for loops.

To illustrate correctness verification for a procedural design, we use a simple example first introduced by Linger, Mills, and Witt. The intent is to design and verify a small program that finds the integer part, y, of a square root of a given integer, x. The procedural design is represented using the flowchart in figure.

To verify the correctness of this design, we must define entry and exit conditions as noted in figure below. The entry condition notes that x must be greater than or equal to 0. The exit condition requires that x remain unchanged and take on a value within the range noted in the figure. To prove the design to be correct, it is necessary to prove the conditions init, loop, cont, yes, and exit shown in figure are true in all cases. These are sometimes called subproofs.

**1.**The condition init demands that [x ≥ 0 and y = 0]. Based on the requirements of the problem, the entry condition is assumed correct. Therefore, the first part of the init condition, x ≥ 0, is satisfied. Referring to the flowchart, the statement immediately preceding the init condition, sets y = 0. Therefore, the second part of the init condition is also satisfied. Hence, init is true.

**2.**The loop condition may be encountered in one of two ways:

**(1)**directly from init (in this case, the loop condition is satisfied directly) or via control flow that passes through the condition cont. Since the cont condition is identical to the loop condition, loop is true regardless of the flow path that leads to it.

**3.**The cont condition is encountered only after the value of y is incremented by 1. In addition, the control flow path that leads to cont can be invoked only if the yes condition is also true. Hence, if (y + 1)2 ≤ x, it follows that y2 ≤ x. The cont condition is satisfied.

**4**. The yes condition is tested in the conditional logic shown. Hence, the yes condition must be true when control flow moves along the path shown.

**5.**The exit condition first demands that x remain unchanged. An examination of the design indicates that x appears nowhere to the left of an assignment operator. There are no function calls that use x. Hence, it is unchanged. Since the conditional test (y + 1)2 ≤ x must fail to reach the exit condition, it follows that (y + 1)2 ≤ x. In addition, the loop condition must still be true (i.e., y2 ≤ x). Therefore, (y + 1)2 > x and y2 ≤ x can be combined to satisfy the exit condition.

We must further ensure that the loop terminates. An examination of the loop condition indicates that, because y is incremented and x ≥ 0, the loop must eventually terminate.

**Advantages of Design Verification**

Rigorous correctness verification of each refinement of the clear-box design has a number of distinct advantages. Linger describes these in the following manner:

**• It reduces verification to a finite process.**The nested, sequential way that control structures are organized in a clear box naturally defines a hierarchy that reveals the correctness conditions that must be verified. An axiom of replacement lets us substitute intended functions with their control structure refinements in the hierarchy of subproofs. For example, the subproof for the intended function f1 in figure requires proving that the composition of the operations g1 and g2 with the intended function f2 has the same effect on data as f1. Note that f2 substitutes for all the details of its refinement in the proof. This substitution localizes the proof argument to the control structure at hand. In fact, it lets the software engineer carry out the proofs in any order.

**• It is impossible to overemphasize the positive effect that reducing verification to a finite process has on quality.**Even though all but the most trivial programs exhibit an essentially infinite number of execution paths, they can be verified in a finite number of steps.

**• It lets cleanroom teams verify every line of design and code.**Teams can carry out the verification through group analysis and discussion on the basis of the correctness theorem, and they can produce written proofs when extra confidence in a life- or mission-critical system is required.

**• It results in a near zero defect level.**During a team review, every correctness condition of every control structure is verified in turn. Every team member must agree that each condition is correct, so an error is possible only if every team member incorrectly verifies a condition. The requirement for unanimous agreement based on individual verification results in software that has few or no defects before first execution.

**• It scales up.**Every software system, no matter how large, has top-level, clear-box procedures composed of sequence, alternation, and iteration structures. Each of these typically invokes a large subsystem with thousands of lines of code—and each of those subsystems has its own top-level intended functions and procedures. So the correctness conditions for these high-level control structures are verified in the same way as are those of low-level structures. Verification at high levels may take, and well be worth, more time, but it does not take more theory.

**• It produces better code than unit testing.**Unit testing checks the effects of executing only selected test paths out of many possible paths. By basing verification on function theory, the cleanroom approach can verify every possible effect on all data, because while a program may have many execution paths, it has only one function. Verification is also more efficient than unit testing. Most verification conditions can be checked in a few minutes, but unit tests take substantial time to prepare, execute, and check.

It is important to note that design verification must ultimately be applied to the source code itself. In this context, it is often called correctness verification.