Constructive specification
= Constructive specification
Specify behavior by constructing a mathematical model and defining the operations on that model. Finite sequences model a <FIFO queue>: insertion appends, the head is the first element, and successful deletion removes it. An <axiomatic specification> can then be checked against the model without requiring the implementation to use that representation.