I worked on program proving from 1968 thru to 1979. I proved all the machine code in my Ph. D. work. All the bugs were in the unproved (Highlevel language) code. Budd's suggested use of invariants very much my published thoughts in the 1970's.
Since the 1970's we have become object oriented and so use classes. Here is how to use the ideas in chapter 5 with a class.
|Part of program||Description||Precondition||Invariant||Postcondition||Result|
|class||Each class should have a set of invariant properties of its attributes (data members). This should be documented in the code.||-||Yes||-||-|
|mutators||Each mutator member function (operation) should have its contract recorded. A contract gives preconditions and postconditions. It is good to record any properties of the attributes are not changed by the function/operation. This part of "Programming by contracts" and the Rational Rose CASE tool.||Yes||Yes||Yes||If not void|
|accessors||Some accessors only work safely under certain conditions. Record them. Also record the value returned in terms of the attributes.||Yes||-||-||Yes|
|bodies||The bodies of functions in object oriented programs tend to be simpler than in older code. Most need little documentation inside.||-||loop||-||-|
|inheritance||If class A is derived from B then every object of type A must also be of type B. You may need to prove that the invariants of A imply those of B. Further each precondition in A should be less restrictive or the same as that in than in B. But each postcondition gets tighter: If function B::f() guarantees a property then A::f() must do the same (and possible more).||looser||tighter||tighter||same|
I researched various forms of Software Quality Assurance (SQA) for the UK Civil Service 1979-1982. I've tracked the topic ever since. I've studied (and used): walkthroughs, inspections, peer review,... etc. .
My research suggests that Budd is wrong to suggest that programmers should defend their code in a walkthrough. Defence wastes time and energy. Further, any piece of code that needs verbal defense needs FIXING! At least better organization, names and comments are needed. Normally some obscure bug needs digging out.
The XP (eXtreme Programming) version of quality conttrol is that all changes to code are made by TWO programmers -- one typing and one thinking about the big picture -- Pair Programming. Bad code is detected fast and fixed before the sun goes down.
Kent Beck (2000) proposes using unit tests as an analysis, design, and implementation tool. To do this you write many unit tests before you right the code. You only change the code if there is a unit test that fails. This is part of the XP process. You may be asked about it in job interviews -- but not in this class. I enjoy doing test first process a lot more than the "analysis, design, code, test " process found in the text books and large safety conscious organizations.
Software Quality Assurance demands other kinds of testing.