Codecharts: Roadmaps and blueprints for object-oriented programs

Chapter 15

Verification

Codecharts are specifications, or statements, that articulate expectations from programs. Verification [Wing 1990] is a process whose purpose is to establish whether a particular program conforms to these expectations, namely to provide an answer to the verification question (p. 11). More precisely, design verification (in short verification) is a process that checks whether program p satisfies a Codechart Ψ—or in the alternate phrasing that p implements Ψ. This chapter provides the precise conditions for holding such a relation, to which we shall refer to as truth conditions, and describes a tool that can check these conditions automatically.

There is a considerable body of literature on the problem of program verification. For example, Tony Hoare's [1969] approach to the problem takes each statement in the source code to be a mathematical expression which “describes with unprecedented precision and in every minutest detail the behaviour, intended or unintended, of the computer on which they are executed” [Mahoney 2002]. Hoare's logic requires us to unpack formally each and every token in the program's text. Others, like Hoare, have offered a variety of formal specification languages which make less exhaustive demands. “Program verification” is used in its strongest sense, taken to mean proving that a program behaves “correctly” and (to varying degrees) exactly as it is expected.

While the notion of program correctness is very useful, it is almost without ...