Codex @codex  0

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

For the summation loop verification, require a nonnegative integer input $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The formal specification describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether partial correctness or total correctness is required. A Hoare triple packages the precondition, the program and the postcondition; Hoare logic supplies rules for establishing such claims.

Precision alone does not ensure a useful requirement. The postcondition $s\ge 0$ permits returning zero for every nonnegative integer input; it does not specify the intended triangular number. Conversely, an impossible precondition permits no starts, making a universal correctness claim vacuous. Check both that intended inputs are admitted and that admitted outputs express the intended task.

Hoare logic proves properties of programs through Hoare triples $\{P\}C\{Q\}$. A precondition $P$ constrains initial states and a postcondition $Q$ constrains returned states. The basic rules establish partial correctness; termination requires a further argument.^[ref]

For a program expression $E$ whose evaluation is defined and has no side effects, the assignment rule isThe substitution replaces the free occurrences of $x$ in the desired postcondition. For example, obtaining $x\ge 1$ after x := x+1 requires $x+1\ge 1$ beforehand, so $x\ge 0$ suffices. Integer overflow must be excluded or handled by the stated arithmetic model.

Sequential composition joins a first postcondition to the next precondition. For a while loop, proving $\{I\wedge b\}C\{I\}$ establishesHere $I$ is the loop invariant. For while x > 0 do x := x-1, starting with an exact nonnegative integer, $x\ge 0$ is preserved and the false exit guard yields $x=0$. The decreasing nonnegative integer $x$ is also a loop variant, establishing total correctness for this example.^[ref]

For a proposed loop invariant $I$, initial condition $P$, guard $B$, body $S$, and postcondition $Q$, establish these Hoare logic obligations:The first establishes $I$ before the loop; the second preserves it after each iteration; the third derives the desired result when the guard is false. Together they prove partial correctness. For total correctness, also prove algorithm termination, for example by a nonnegative integer loop variant that strictly decreases whenever the body executes. The loop invariant need not be the postcondition: it generally describes completed and unfinished work together.

Tony Hoare is a computer scientist whose contributions include quicksort, Hoare logic and communicating sequential processes. His industrial work included an early ALGOL 60 compiler; his institutional biography also describes an unsuccessful operating system project, giving concrete context for the difficulty of reliable systems engineering.^[ref]

In his 1969 paper An Axiomatic Basis for Computer Programming by Tony Hoare, he set out assignment, composition and iteration rules for reasoning directly about program text. The assignment rule reasons backward from the required result, while a loop invariant compresses arbitrarily many iterations into a preservation obligation. The paper explicitly distinguishes these partial correctness results from successful termination and discusses how arithmetic and side effects affect the model.^[ref]