A program describes a computation -- its purpose is to be executed on a computer and perform that computation. Programs are written in a precisely and formally defined programming language, e.g., Java, C, Pascal. A program specification describes the results that a program is expected to produce -- its primary purpose is to be understood not executed. Specifications provide the foundation for programming methodology.
A specification is a technical contract between a programmer and his/her client and is intended to provide them with a mutual understanding of a program. A client uses the specification to guide his/her use of the program; a programmer uses the specification to guide his/her construction of the program. A complex specification may engender sub specifications, each describing a sub component of the program. The construction of these sub components may then be delegated to other programmers so that a programmer at one level becomes also a client at another.
Experience shows that it is extremely challenging to create high quality software. A clearly understandable specification is a vital ingredient in the creation process. English has proven to be too vague, verbose and ambiguous to rely on for the necessary precision. Of course, the program itself determines what results are produced, so it may be regarded as the ultimate specification. However, the program is available only at the conclusion of the programmer-client interaction, and cannot be a factor in developing a suitable initial contract. And even when it is completed, the plethora of details in programs overwhelms a clear understanding and disqualifies the program from serving the purposes of a specification.
The purpose of a specification requires that all parties have complete confidence in the properties of the results it warrants. The focus of a specification should be on what is achieved, not how it is achieved -- the details engendered in the program itself are to be avoided. Precise and formally defined conventions for writing specifications are a much more recent invention than programming languages. The need to be fully precise about results before beginning the programming process has lead to a reliance on mathematically based (or more accurately, logically based) concepts.
Since a specification provides a technical contract, it is only natural to base both the construction and the verification of a program on its specification. As a result "formal methods" subsumes: (i) conceptual elements for the development of precise specifications that can serve to guide programming activity, (ii) the means to utilize a formal specification for a rigorous verification of the program when it is completed, and (iii) the integration of these ideas into a "system of specification" that can be supported by computer-based tools that assist the entire enterprise. It is this view that guides our course.