Sequence-based software specification

The primary result of this research is the sequence enumeration method of specifi-cation writing. Straightforward, systematic enumeration of all sequences to pro-duce an arguably complete, consistent, and correct specification is made practical by a collection of techniques based on controlling the growth of an inherently combinatorial process. By systematic investigation of stimulus histories, regular expression "rules" can be discovered and mapped to responses. These rules can be used to partition the set of all stimulus histories, providing an arguably complete, consistent, and correct black box specification. Computable predicates and other refinements are used where regular expressions are insufficient to capture behavior. Using derivatives of regular expressions, a minimum-state recognizer can be created for each regular block of the black box. These recognizers can be com-bined by direct product into a sequential machine which is then minimized. The resulting sequential machine is a faithful representation of the original specifica-tion. The production of the sequential machine provides verification of the com-pleteness and consistency of the original specification. Through the introduction of state variables, the state machine's state space is partitioned until every state can be specified by giving values for each of the state variables. A language for state boxes is introduced, and a sequential machine whose state space has been properly partitioned can be automatically trans formed into a state box. State migration issues are discussed as they arise during the distribution of the sequential machine's state space.