O'Reilly logo

Codecharts: Roadmaps and blueprints for object-oriented programs by J. Nicholson, Amnon H. Eden

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required