Ntu weekly Lesson Topic Worksheet

Lectures 24 and 25

More Functional Verification “Magic” and an Overview of Cleanroom Software Engineering
We conclude our study of functional verification this week by briefly considering a remarkable connection between the functions computed by programs with while loops and the loop invariants studied in Lecture 18 (“Functional Verification IV: Revisiting Loop Invariants”). In particular, we will see how the Invariant Status Theorem (IST) provides a way to systematically derive “f-adequate” loop invariants when the function, f, computed by the loop is known! As illustrated in the paper by Dunlop and Basili, the IST is closely related to the observation that a loop computing f maintains an important property of state across iterations: the function value of the current state, X, is the same as the function value of the initial state, X₀ – i.e., f(X)=f(X₀). Finally, we consider a paper written by Harlan Mills associate Rick Linger about an interesting and somewhat controversial SE development method that utilizes function-theoretic verification: “Cleanroom Software Engineering.”

Week 13 – Functional Verification IV

Context:

In Week 10 we learned that synthesizing a loop invariant is a trial-and-error process. We now consider a way to systematically derive loop invariants when the function computed by the loop is known.

Purpose:

To introduce and illustrate the application of the Invariant Status Theorem in deriving f-adequate loop invariants. Depending on the relationship between a specified post-condition, Q, and a program’s actual function, f, these invariants may in some cases be used with the while loop ROI to prove the correctness of while_do statements. Since in many situations, a loop invariant may hold by virtue of its initialization, we also consider a limited invariant of an initialized while loop: h; while p do g.

Competency Objectives:

At the end of this lesson, you will be able to:

1. 
   State and apply the Invariant Status Theorem to derive an invariant, q(X), for a simple while loop with a known function.
   
2. 
   Derive a limited invariant for an initialized while loop with a known function.
   

Key Points:

1. 
   Invariant Status Theorem: Let f = [while p do g]. If X₀∈D(f), X∈D(f), and q(X)=( f(X)=f(X₀) ), then q is an invariant of while p do g, and has the following properties:
   

1. 
   q(X₀) is true, and
   
2. 
   (q(X) Л p(X)) Þ qog(X), and
   
3. 
   (q(X) Л ¬p(X)) Þ (X=f(X0))
   

2. 
   To expand on the unique nature of q(X), note that the set of states satisfying f(X)=f(X₀) includes all intermediate states that could possibly be generated by any while loop that computes f!
   

3. While Loop Initialization: Given f = [while p do g], X₀ ∈ D(f), a limited

invariant of the initialized while loop: h; while p do g is:

q(X) = ( f(X)=foh(X₀) )

Such an invariant has the following properties:

1. 
   qoh(X₀) is true, and
   
2. 
   (q(X) Л p(X)) Þ qog(X), and
   
3. 
   (q(X) Л ¬p(X)) Þ (X = foh(X₀))
   

Cleanroom Software Engineering

Context:

Cleanroom Software Engineering is a software development philosophy first introduced in the 1980s within IBM by Harlan Mills. It is based on the notion that defects in software should be avoided rather than detected and repaired. Development teams employ function-theoretic correctness verification techniques.

Purpose:

To briefly describe a successful use of formal verification techniques in a practical, scalable software development method.

Competency Objectives:

At the end of this lesson, you will be able to:

1. 
   State the underlying philosophy of Cleanroom Software Engineering.
   
2. 
   Describe important characteristics of Cleanroom, including "box structure" specification and design, incremental development, and statistical usage testing.
   

Key Points:

1. 
   Cleanroom Software Engineering is based on the notion that defects in software should be avoided rather than detected and repaired. Software development should not be viewed as a trial-and-error undertaking.
   
2. 
   Cleanroom makes use of function-theoretic correctness verification – components are not executed or developer-tested!
   
3. 
   “Every correctness condition of every control structure is verified – every team member must agree that each condition is correct.”
   
4. 
   Statistical usage testing utilizes a sample population of user executions based on expected frequency. Quality is measured by determining if executions are correct
   
5. 
   Box structure specification and design incorporates black box (external behavior), state box (retained data), and clear box (processing) forms.
   

Self-Check Quiz Questions

1. 
   (6 pts.) For program P below, use the Invariant Status Theorem to synthesize a limited invariant that COULD be used to prove that the program is weakly correct with respect to pre-condition {true} and post-condition {y=x-k} using the while loop rule of inference.
   

y := 0

t := x

while t<>k do

t := t-1

y := y+1

end_while

2. 
   (4 pts.) In "Cleanroom Software Engineering for Zero-Defect Software," Linger claims that statistical usage testing is "more that 20 times more effective" than coverage testing at doing something. What is it more effective at doing, and why is this so?