Codecharts: Roadmaps and blueprints for object-oriented programs

Chapter 18

Reasoning About Charts

Visual representations of evidence should be governed by principles of reasoning… Clear and precise seeing becomes as one with clear and precise thinking.

—Edward R. Tufte

In this chapter we examine some simple means for reasoning about Codecharts. Having formalized the relation between charts and programs, we revisit the problem of abstraction (Chapter 1) and introduce a set of abstraction operators which allow us to reason rigorously about Codecharts. This shall allow us to formulate precisely the relation between charts that are similar in some sense and draw sound conclusions on the relations between design patterns.

In the first part of this book we made informal claims of the form “chart Ψ is an abstraction of chart Φ” and “chart Φ is a special case of chart Ψ”. One way of understanding such claims is that “every program that implements Φ also implements Ψ.” The formal definitions provided in this part of the book allow us to make this intuitive notion precise with relative ease.

Precisely put, given specifications Φ and Ψ, we say that Φ semantically entails Ψ (Definition XIX), written

Φ Ψ

if and only if every design model that satisfies Φ also satisfies Ψ.

Corollary 1. The semantic entailment relation is transitive: If Φ Ψ and Ψ Δ, then ...