Browse Prior Art Database

Formal Specification As a Design Tool

IP.com Disclosure Number: IPCOM000128890D
Original Publication Date: 1980-Dec-31
Included in the Prior Art Database: 2005-Sep-20
Document File: 16 page(s) / 49K

Publishing Venue

Software Patent Institute

Related People

John Guttag: AUTHOR [+4]

Abstract

The formulation and analysis of a design specification is almost always of more utility than the verification of the consistency of a program with its specification. Good specification tools can assist in this process, but have generally not been proposed and evaluated in this light. In this paper we outline a specification language combining algebraic axioms and predicate transformers, present part of a non-trivial example (the specification of a high-level interface to a display), and finally discuss the analysis of this specification. CR Categories: 4.0, 4.6, 5.24 Key words and phrases: Formal specification, algebraic axioms, design validation tMIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139. Supported in part by the National Science Foundation under grant MCS78-01798 and by an, Office of Naval Research Contract with DARPA funding #NO0014-75-C-0661. To be presented at Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, Jan. 28-30, 1980.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 8% of the total text.

Page 1 of 16

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Formal Specification As a Design Tool*

by John Guttag and James J. Homing

CSL-80-1 January 1980

Abstract:

The formulation and analysis of a design specification is almost always of more utility than the verification of the consistency of a program with its specification. Good specification tools can assist in this process, but have generally not been proposed and evaluated in this light. In this paper we outline a specification language combining algebraic axioms and predicate transformers, present part of a non-trivial example (the specification of a high-level interface to a display), and finally discuss the analysis of this specification.

CR Categories: 4.0, 4.6, 5.24

Key words and phrases: Formal specification, algebraic axioms, design validation

tMIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139. Supported in part by the National Science Foundation under grant MCS78-01798 and by an, Office of Naval Research Contract with DARPA funding #NO0014-75-C-0661.

To be presented at Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, Jan. 28-30, 1980.

XEROX PALO ALTO RESEARCH CENTER

3333 Coyote Hill Road / Palo Alto / California 94304

Introduction

There are at least three distinct concerns in the software development process:

1) Developing an intuitive understanding of the problem to be solved. This should involve extensive discussions with members of the anticipated user community, and an examination of any existing software or manual procedures designed to deal with similar problems.

2) Designing a system intended to solve that problem. This may involve multiple iterations, in which partial designs are proposed and carefully analyzed for consistency, completeness, and conformance with intuition.

3) Programming an implementation of the design. This may also involve multiple iterations, in which portions of the program are developed and carefully analyzed for legality, efficiency, and conformance with the design.

Xerpx Palo Alto Research Center Page 1 Dec 31, 1980

Page 2 of 16

Formal Specification As a Design Tool

In practice, these concerns are never totally separated, nor entirely sequential. Each process is guided by expectations about subsequent processes. Furthermore, the understanding, the design, and (to a lesser extent) the program will generally evolve together, as each analysis provides feedback to previous steps, and as some sort of validation process is undertaken as part of each step.

We have frequently concentrated our attention on the tail end of this process. An obvious symptom of this is the tremendous amount of attention we have lavished on the design of programming languages. A less obvious symptom has been the effort expended on "program" verification, i.e., on demonstrating the consistency of the result of the second step with the result of the third.

Curiously, many of us working in the areas of progr...