Codecharts: Roadmaps and blueprints for object-oriented programs

Part II

Theory

The design of computing systems can only properly succeed if it is well-grounded in theory, and … the important concepts in a theory can only emerge through protracted exposure to application.

—Robin Milner

It has long been my personal view that the separation of practical and theoretical work is artificial and injurious. Much of the practical work done in computing, both in software and in hardware design, is unsound and clumsy because the people who do it have not any clear understanding of the fundamental design principles of their work. Most of the abstract mathematical and theoretical work is sterile because it has no point of contact with real computing.

—Christopher Strachey

This part offers a rigorous foundation for LePUS3, the language of Codecharts. We define precisely the relation between programs and specifications, and provide an answer to the verification question. We also describe Class-Z, an equivalent specification language to LePUS3. We conclude with the subject of reasoning on Codecharts.

Most formal statements provided in this chapter (propositions and lemmas) will include sketched “proofs”, the simplest of which will be omitted. Formal definitions can be found in Appendix II.

NOTATIONAL CONVENTIONS

The following writing conventions are adopted throughout this chapter:

• If is shorthand for “if and only if”
• The notation {a, b} denotes a set with two elements a and b.
• Given a set T, we use to denote the set of all subsets of T (the power set ...