Skip to content
Hamilton Archive
0 / 17
Pre-launch Review

Higher Order Software -- A Methodology for Defining Software

Higher Order Software — A Methodology for Defining Software

Section titled “Higher Order Software — A Methodology for Defining Software”

Margaret H. Hamilton and Saydean Zeldin, Charles Stark Draper Laboratory, 1976

Higher Order Software is defined as “a formal methodology for reliable systems specification and development.” The foundational insight is that software must be defined as hardware-independent, language-independent, and computer-resident-software-independent. HOS concerns itself only with “computable functions and their relationships,” adopting the Church-Turing definition: a function is effectively computable if there is a mechanical and finite method of calculating the value of the function in all cases when its arguments are given.

The critical empirical finding that drives the entire paper appears in a footnote on page one: “Seventy-three percent of all problems found during the APOLLO integration effort were interface problems; and verification accounts for 50 percent of the total software development effort.” This 73% figure — later rounded to 75% in subsequent publications — became the empirical anchor for the entire HOS program and the decades of work that followed.

The Six Axioms of Control

Section titled “The Six Axioms of Control”

Any software system is represented by a single mathematical function with input domain and output range. The system function is an assumption; subfunctions are derived. The six axioms describe “control” — the formally specified effect of one software object on another.

Axiom 1 (Invocation): A module controls invocation of functions on its immediate, and only its immediate, lower level. The module cannot control invocation on its own level or of its own function. This immediately implies the “no GOTO” property of structured programming and prevents circular invocation.

Axiom 2 (Responsibility): The module controls the responsibility for elements of the output space. There must not exist any member of the input space for which no member of the output space is assigned — totality of the function.

Axiom 3 (Output Access Rights): The module controls access rights to output variables for each immediate lower-level function.

Axiom 4 (Input Access Rights): The module controls access rights to input variables for each immediate lower-level function. The module cannot alter its own input set.

A key theorem derived from Axioms 3 and 4: the output set of a function cannot be the input set of that same function. This eliminates an entire class of side-effect errors.

Axiom 5 (Rejection): The module can reject invalid elements of its own, and only its own, input set. This formalizes error detection as a first-class concern.

Axiom 6 (Ordering): The module controls the ordering of each tree for the immediate lower level. This governs priority relationships for real-time processes, including a theorem that a process cannot interrupt itself and that the WAIT statement is inconsistent with the control system.

Interface Correctness

Section titled “Interface Correctness”

Interface correctness is defined as “a property of a system which results in the ability to perform a function without ambiguity.” It is proven by showing axiom consistency. The paper carefully distinguishes interface correctness (provable by HOS) from performance correctness (the “does the algorithm do the right job?” question, which requires testing or formal proof). Of Apollo errors, 13% were performance specification errors; 73% were interface errors. HOS targets the 73%.

Specification Language Principles

Section titled “Specification Language Principles”

The HOS specification language separates system performance properties from interface correctness properties. It is not primarily a language for computer execution but for reliable system decomposition. Three levels of checking are defined: assembler (instruction level), compiler (statement level), analyzer (interface specification level).

The nodal family — a node and its immediate lower-level nodes — is the fundamental unit of decomposition. Two primitive decomposition types form the basis:

  • Partition: Divides input elements or output variables. Two subtypes exist: selection partition (divides elements of the input set, each subfunction produces all output variables) and class partition (divides output variables, all subfunctions performed for every input).
  • Composition: Communication between subfunctions on one level. Variables flow from one subfunction through intermediate variables to another.

The paper formally proves that if A then B (without else) is invalid in HOS because it creates an incomplete partition. The while A do B construct is invalid because it can alter its own input set, violating Theorem 3,4.1. Recursion replaces iteration through a combination of composition and partition.

Error detection and recovery are formalized: errors occur when output is undefined; detection occurs when input is invalid (maps to Reject). Recovery is always provided by the controller, not the function itself. The “P unless error then refresh P” construct enables system-wide restart — a direct formalization of Apollo’s restart capability.

The Design Analyzer and Structuring Executive

Section titled “The Design Analyzer and Structuring Executive”

Two analyzers form the core tooling:

The Design Analyzer (static analysis) operates in four phases: (1) check interface correctness, (2) determine where performance testing is needed, (3) analyze timing and memory per level, and (4) automatically program from HOS to intermediate language or execution.

The Structuring Executive Analyzer (dynamic/real-time) handles the man/machine interface, hardware/software interface, error detection/recovery, real-time reconfiguration, and dynamic allocation. The key principle: “the human can select any reconfiguration of nodes in real time without concern for introducing errors into the system.”

The two analyzers are functionally equivalent: the Design Analyzer does statically what the Structuring Executive does dynamically.

Software Management

Section titled “Software Management”

The Apollo statistical analysis yielded additional findings beyond the 73%: 44% of anomalies were found by “eyeballing” (manual inspection); no pure software problems occurred in any Apollo flight; the AGC systems software (scheduler, display interface, restart modules) had zero interface problems during integration — all 73% of interface errors were between application modules.

Hamilton and Zeldin establish that the management structure should mirror the software structure one-to-one. Managers at the same level do not determine interfaces with each other — interfaces are set by the higher-level manager. This is a direct formalization of the Apollo management structure.

Results

Section titled “Results”

HOS was applied to: Shuttle Flight Software Requirements Integration (partial axiom application) and DAIS avionics (full HOS definition of requirements, link editor, and federated multiprocessor operating system). The automatic structured design diagrams were operational. A prototype HOS Analyzer was under development, translating HAL source code to HOS control descriptions.

Counter to expectations, HOS structuring often produced more efficient code than conventional methods. The recommendation: always structure at the functional level using axioms; design as if communicating with an asynchronous executive. “It is hoped that someday solutions to efficiency problems will be more powerful hardware, rather than a compromise of software reliability.”

Hamilton predicted: “Someday, the only phase that should be required for software development will be Phase 1” — the definition of functions and interfaces.

References

Section titled “References”

The paper contains 22 references including Hamilton’s internal Draper Laboratory memos and notes, the 1974 Springer conference paper presenting the axioms, and related work on structured programming and formal methods.

Section titled “Related Documents”