45 ;;Quote: programmers should be required to use engineering practices that prevent latent execution failures

45+;;Quote: via functional verification inspections, the IBM Wheelwriter had no software errors after 6 years; 63 Kloc of code on three processors

46 ;;Quote: unit verification by debugging may cause design faults when the fixed modules are combined

46 ;;Quote: in most cases, the cause of a software product failure was introduced while fixing another failure

47 ;;Quote: functional verification structures a proof that a program implements its specification correctly

47 ;;Quote: functional verification leaves 2-5 fixes/Kloc for later phases compared to 10-30 fixes/Kloc from unit testing

48 ;;Quote: statistical usage testing is 21 times more effective than coverage testing because most errors are seldom observed

49 ;;Quote: Codd developed relational databases to solve data-maintenance abnormalities due to failures in referential transparency

49 ;;Quote: Cleanroom engineering uses teams for specification, development, and certification

50 ;;Quote: an internal specification defines responses in terms of stimuli histories; avoids commitment to an implementation

50+;;Quote: representing prior stimuli by state data (invented abstractions) specifies an implementation

51 ;;Quote: statistical testing by selecting tests according to a usage profile

51+;;Quote: develop an expected usage profile with a Markov model on usage states and estimated transition probabilities

51 ;;Quote: should have user-level commands for each increment in a construction plan; top-down, no special testing routines, helps estimate MTTF

51 ;;Quote: Cleanroom's development team designs each increment top-down with usage hierarchy, black-box, state-box, and clear-box

51+;;Quote: Cleanroom's development team implements clear boxes by stepwise refinement and verifies each function

51 ;;Quote: Cleanroom's black-box view defines system responses in terms of stimuli histories; implementation-independent

51 ;;Quote: Cleanroom's state-box view defines system responses in terms of state data and the current stimuli; data-driven, captures stimuli history

51 ;;Quote: Cleanroom's clear-box view defines system responses in terms of lower level black boxes, data abstractions for states, and current stimuli; process-driven

51 ;;Quote: both data (state-boxes) and process (clear-boxes) views are needed for designing software; related by box structures

51 ;;Quote: verify state-box descriptions by eliminating references to state data; should match the original black-box function

52 ;;Quote: verify clear-box descriptions by eliminating references to lower level black boxes; should match the original state-box function

52 ;;Quote: verify the expansion of a clear-box into code by constructing a proof argument that the expansion matches the functional specification

52+;;Quote: using Cleanroom techniques, can construct proof arguments for very large software systems

53 ;;Quote: Cleanroom's certification team adds an increment to previous increments and measures its MTTF with random test cases

53+;;Quote: Cleanroom's certification team estimates MTTF for the next version; force a redesign if failures are too frequent or serious