Specification: before the code is written

What an algorithm's specification must hold so that an implementer, a person or a model, builds it correctly: the contract first, code-like steps, and examples that become the first tests. The shape is the algorithm specification.

Principle	Claim
Contract before steps	the precondition and postcondition come before the steps
Code-like steps	the steps are constrained pseudocode, not prose
Examples and properties as tests	examples with expected outputs, edge cases first, and properties for every input