Diagramming and Spatiality

I am deeply interested in diagrams, particularly in how they enable thinking, theorizing, exploration, and communication.

“Spatial thinking is the foundation of abstract thought.” — B. Tversky

The most important aspect of a diagram is how it is spatially arranged, not its aesthetic rendering. I am interested in understanding the spatial operations that are needed to build useful¹ diagrams.

I am, however, not a cognitive scientist, a designer, or a psychologist. Informed by my background in programming languages, software engineering, and formal methods, I aim to operationalize the insights of these disciplines via a programming language-based approach.

Diagramming by Specification

The key difference between a program and a specification lies in how they relate to behavior. An empty program performs no actions – it exhibits no behavior whatsoever. In contrast, an empty specification allows all possible behaviors, since it imposes no constraints. In a lightweight specification language like Forge, this means that an empty spec permits every conceivable structure or behavior, simply because nothing has been ruled out.

A program defines exactly what should happen, whereas a specification describes what is required.

Cope and Drag: Lightweight Diagramming for Lightweight Formal Methods

Cope and Drag is a diagramming-by-specification programming language designed for use with the Forge lightweight formal methods² tool.

A central attribute of lightweight formal methods is that users can reason informally about their designs before doing so formally. Whereas traditional verification tools require properties before the tools can do anything effective, tools like Forge can work with just system descriptions. They use a SAT-solver to generate instances of the system and present these to the user, most commonly in visual form.

This has two benefits:

1. Users can (hopefully quickly) spot ways in which the output does not conform to their intent, and improve their specification.
2. Seeing these violations suggests desirable and undesirable properties, which can then be formalized and turned into verification conditions.

Thus, realizing lightweightness hinges heavily on the quality of visualizations. In turn, once properties exist, counterexamples to their success are also presented using the same mechanisms.

Cope and Drag leverages this default visualization to enable diagramming by refinement.

• An empty Cope and Drag spec starts with the default Forge visualizer’s output.
• As users progressively add constraints and directives, the diagram is selectively refined, making it more relevant and expressive for the user’s needs.

This design provides a middle ground between purely programmatic approaches (which allow fine control but can be labor-intensive) and pure genericity. Additionally, unlike optimization-focused based diagramming languages (e.g., Penrose, BlueFish), a diagram is only generated if the Cope and Drag specification does not conflict with instances generated by the Forge model. This makes Cope and Drag a meaningful debugging tool, as it produces a solver-generated ‘‘core’’ of conflicting diagramming primitives for these bad instances.

See more details about Cope and Drag here

🔍 See our upcoming paper in ECOOP 2025.

Related Publications