Hamilton & Zeldin (1979): Design and Verification

Source

Hamilton, Margaret H. and Saydean Zeldin, “The Relationship Between Design and Verification,” Journal of Systems and Software, Vol. 1, 1979, pp. 29-56. DOI: 10.1016/0164-1212(79)90004-9.

Charles Stark Draper Laboratory (formerly MIT Instrumentation Laboratory), Cambridge, Massachusetts.

Download PDF

The 1976 paper defined six axioms and argued that structurally correct software prevents interface errors by construction. This paper answers the obvious follow-up: how do you check axiom compliance, and what do you do once you have a verified design?

The answer is AXES — the Automated eXtensibility and Evaluation System. It takes a system specification expressed as HOS control maps, checks all six axioms mechanically, and generates executable code from compliant specifications. Where the 1976 paper was a theory, this paper is a tool.

The Core Argument

Design and verification are conventionally sequential: design something, build it, then test whether it works. Hamilton and Zeldin argue this ordering is wrong. If the design methodology itself guarantees structural correctness, then verification of structural properties is complete the moment the design passes axiom checking. What remains is testing leaf computations — the individual algorithms within primitive operations — against their specifications.

The paper states this as a proportion. Interface errors, control flow errors, and type errors account for 60-70% of defects in large systems (a figure carried from the 1976 paper’s IBM citations). HOS axioms eliminate these categories at design time. The remaining 30-40% — incorrect algorithms within correctly-structured modules — are the only things that need conventional testing.

The slogan: you cannot test quality in. You have to design it in.

AXES: The Tool

AXES has three capabilities:

1. Specification Analysis

Given a control map expressed in HOS notation, AXES checks all six axioms:

Axiom	What AXES Checks
Ordering	Parent controls child invocation sequence; no child alters it
Input/Output	Every function’s interface is complete — no hidden data flow
Access	Data access matches hierarchical position — no unauthorized reads/writes
Connection	Every input has a source, every output has a destination
Type	Operations on data are consistent with declared types
State Change	Modifications are visible only through declared outputs

Violations are reported with the offending function, the specific axiom, and the data flow or control path that violates it. The checking is mechanical — no human judgement required, no “it looks right” assessments.

2. Code Generation

If the specification passes all axiom checks, AXES generates executable code. The mapping is direct:

HOS Structure	Generated Code
JOIN	Sequential block
OR	Conditional (IF-THEN-ELSE)
INCLUDE	Subroutine call
Leaf operation	Primitive code template
Data connections	Parameter passing

The generated code preserves the hierarchy of the specification. Every line traces back to a specific node in the control map. This traceability is itself a verification property: if the specification is correct and the generator is correct, the generated code is correct by construction.

The paper demonstrates FORTRAN generation, though the authors note the target language is arbitrary — the specification is language-independent.

3. Extensibility

New primitive operations can be added to the system by defining their interface (inputs, outputs, types) and providing an implementation. AXES checks that new primitives are consistent with the existing type system before accepting them.

Worked Examples

The paper devotes substantial space to demonstrating the AXES workflow:

Navigation computation (pp. 35-40) — A multi-step calculation specified as a control map, axiom-checked, and code-generated. An access violation (a function reading data outside its granted scope) is caught during specification analysis before any code exists.

Scheduling system (pp. 41-48) — A system with conditional execution (OR structures) and shared data. Connection integrity violations (orphaned outputs with no destination) are detected in the control map.

Error injection (pp. 48-52) — Deliberate axiom violations introduced into a correct specification to exercise AXES diagnostics. Each violation type produces a specific error message that names the axiom, the offending function, and the problematic data flow.

The Navigation Example

The choice of a navigation computation as the first worked example is not accidental. Hamilton’s team built navigation software for Apollo. The example demonstrates HOS on familiar ground — the kind of system where interface errors have consequences measured in human lives.

Where HOS Sits

The paper positions HOS between two verification traditions:

Informal methods — flowcharts, natural language specifications, code reviews. Expressive and flexible, but verification requires building and running the software. Errors found late.

Formal proof — Floyd-Hoare verification, algebraic specification. Rigorous, but proof complexity grows faster than system complexity. Practical for individual procedures, impractical for large systems.

HOS occupies a middle ground: formal enough for mechanical checking, but operating at the system-structure level rather than the statement-by-statement level. The axioms constrain the architecture of the system, not the implementation of each line. Since most errors are architectural (interface, control flow, access), this is the right level of abstraction for the largest return.

Scope of Claims

The paper’s error-reduction claims rest on the 1976 IBM citation (60-70% of errors are interface-related). Hamilton and Zeldin do not present empirical data comparing HOS-developed systems against conventionally-developed systems in this paper. That empirical validation came later, in work at Hamilton Technologies through the 1980s and 1990s. The 1979 paper demonstrates that AXES works (it checks axioms and generates code), not that it produces measurably better outcomes at scale.

The Full Arc

This paper completes a trajectory that starts at the Apollo Guidance Computer:

1. Hoag (1963) defines the G&N system architecture — sensors, computer, displays, and the philosophy that automation serves the operator
2. R-393 (1963) documents the AGC architecture that Hamilton’s team would program — the priority executive, the memory structure, the interrupt handling
3. Apollo missions (1968-1972) — the flight software works, survives emergencies, and reveals which structural properties matter most
4. Hamilton & Zeldin (1976) formalizes those structural properties into six axioms
5. Hamilton & Zeldin (1979) [this paper] makes the axioms mechanically checkable and generates code from verified specifications

Step 5 is the transition from craft to engineering. The knowledge is no longer in the heads of the people who built Apollo — it is in a tool that can be applied to any system.

Hamilton would continue developing these ideas at Hamilton Technologies, Inc. (founded 1986), where HOS evolved into the “Development Before the Fact” methodology and the Universal Systems Language (USL). The 2008 capstone paper traces this full arc — from Apollo flight software through HOS axioms to USL’s formal foundations — and presents the empirical finding that 75% of errors in the systems Hamilton’s team analyzed were interface errors, the exact category HOS axioms eliminate by construction.

---

Hamilton & Hackler (2008): Universal Systems Language The capstone -- tracing Apollo through HOS to USL's formal foundations, with the 75% interface error finding

Hamilton & Zeldin (1976): Higher Order Software The predecessor -- six axioms for structurally correct software

Hoag (1963): Apollo G&N The system whose flight software experience motivated HOS

Space Software Engineering Collection overview and document inventory