abstract ;;Quote: document a program with a set of independent displays, a lexicon, and an index; each display gives specification, program, and specifications of invoked programs

948 ;;Quote: since a successful program will be read more often than written, review and maintenance are at least as important as design

948 ;;Quote: a program is correct if it is correct when each part is correct, and if each part is correct

949 ;;Quote: documentators usually focus on the details that look difficult; but readers find that the basic structure is not obvious and the details are overwhelming

949 ;;Quote: the decomposition phase of the review process should be communicated by the designer; the reviewer should not need to derive the decomposition

950 ;;Quote: a well-structured program can always be written as a short text that names other programs that are themselves short

950+;;Quote: with displays, a program made of many short programs can be checked one display at a time

953 ;;Quote: a display is a 1-2 page document with a specification, a program, and all referenced specifications

953 ;;Quote: automatically construct a program from displays by calling procedures and expanding macros

953 ;;Quote: use a lexicon to define terms, functions, constants, and types that are used in multiple displays

953 ;;Quote: use tables to specify the post-value of a variable for various combinations of pre-values

953+;;Quote: an 'NC' entry specifies that the variable is not changed for that combination of pre-values

958 ;;Quote: used displays to inspect safety-critical software for a nuclear plant

958+;;Quote: the tabular organization of displays allowed a step-by-step review process

961 ;;Quote: checked that the displays satisfied the requirements document by transforming the display's tables into the corresponding requirement tables

966 ;;Quote: since programs can only be understood in small chunks, they should always be presented in complete, small pieces