A Technique for Software Module Specification with Examples

Motivation(s)

A growing problem in software engineering is the lack of technique for precisely specifying program segments without revealing too much information.

Proposed Solution(s)

The author proposes viewing a program module as a device with a set of switch inputs and readout indicators, whose values are completely determined by the previous values of the indicators and input positions.

Evaluation(s)

The technique have been evaluated successfully with small systems in an undergraduate course.

Future Direction(s)

  • Is it possible to use code documentation (e.g. Sphinx) to derive TLA capabilities, workflow validation, and unit test generation?

Question(s)

  • Which modern language use machine checkable comments to describe exceptions and assertions?

Analysis

A set up of guidelines to produce high quality system documentation, which in turn can be used to automatically check system integrity. It is unfortunate that TLA-like comments have not been adopted. It would be interesting to see if these guidelines are enforceable under hard deadlines.

Notes

Goal of Specification

  1. Provide the intended user with all the information to use the program correctly, and nothing more.

  2. Provide the implementer all the information about the intended use that is needed to complete the program, and nothing more.

  3. Information can be machine tested for consistency.

  4. Discuss the program in the terms normally used by user and implementer alike.

Two Types of Functions

  1. Provide information which cannot be determined without calling that function unless the user manually maintains duplicate information.

  2. Mapping functions provide redundant information.

    • The value of these functions is completely predictable from the current values of other functions.

Specification

  • Set of possible values

  • Initial Values

    • Undefined is considered a special value instead of an unpredictable value.

  • Parameters

  • Effects (e.g. state, errors, trap, assertions, machine checkable comments)

References

Par72

David Lorge Parnas. A technique for software module specification with examples. Communications of the ACM, 15(5):330–336, 1972.