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 “fadequate” 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_{0} – i.e., f(X)=f(X_{0}). Finally, we consider a paper written by Harlan Mills associate Rick Linger about an interesting and somewhat controversial SE development method that utilizes functiontheoretic verification: “Cleanroom Software Engineering.”
Week 13 – Functional Verification IV
Context:
In Week 10 we learned that synthesizing a loop invariant is a trialanderror 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 fadequate loop invariants. Depending on the relationship between a specified postcondition, 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:

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

Derive a limited invariant for an initialized while loop with a known function.
Key Points:

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

q(X_{0}) is true, and

(q(X) Л p(X)) Þ qog(X), and

(q(X) Л ¬p(X)) Þ (X=f(X0))

To expand on the unique nature of q(X), note that the set of states satisfying f(X)=f(X_{0}) 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_{0} ∈ D(f), a limited
invariant of the initialized while loop: h; while p do g is:
q(X) = ( f(X)=foh(X_{0}) )
Such an invariant has the following properties:

qoh(X_{0}) is true, and

(q(X) Л p(X)) Þ qog(X), and

(q(X) Л ¬p(X)) Þ (X = foh(X_{0}))
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 functiontheoretic 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:

State the underlying philosophy of Cleanroom Software Engineering.

Describe important characteristics of Cleanroom, including "box structure" specification and design, incremental development, and statistical usage testing.
Key Points: 
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 trialanderror undertaking.

Cleanroom makes use of functiontheoretic correctness verification – components are not executed or developertested!

“Every correctness condition of every control structure is verified – every team member must agree that each condition is correct.”

Statistical usage testing utilizes a sample population of user executions based on expected frequency. Quality is measured by determining if executions are correct

Box structure specification and design incorporates black box (external behavior), state box (retained data), and clear box (processing) forms.
SelfCheck Quiz Questions

(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 precondition {true} and postcondition {y=xk} using the while loop rule of inference.
y := 0
t := x
while t<>k do
t := t1
y := y+1
end_while

(4 pts.) In "Cleanroom Software Engineering for ZeroDefect 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?
Dostları ilə paylaş: 