A practical view of program development

Ideally, a specification is only a description of what a program does, and an explanation of how to use that program. A specification should faithfully capture the informal intentions. Such specifications are totally declarative in that they don t express how the program actually works, and they thus don t bias the programmer in her/his task. Specifications have been alternately required to be not (necessarily) executable [Hayes and Jones 89], (preferably) executable [Fuchs 92ab], and so on 

Desirable qualities of a specification language are expressiveness (provision of constructs that are natural to human thinking in the application domain) and readability. 

A crucial aspect of a specification is its total correctness with respect to the informal intentions. Total correctness is often divided into partial correctness (absence of contradictions with the intentions) and completeness (absence of under-specification). While partial correctness of a specification with respect to the intentions is often only assumed (even if this is often far from obvious), such is not the case with completeness, and hence with total correctness. 

Other desirable qualities of a specification are minimality (absence of overspecification), internal consistency (absence of internal contradictions), nonambiguity (existence of a single interpretation), and non-redundancy (absence of synonymy, homonymy, and so on). 

A specification language should offer abstract data-types, so that specifications do not bias the algorithm design or implementation processes. However, abstract datatypes and the issue of their reification are not addressed anywhere in this book. 

---