A Sampler of Formal Definitions
Michael Marcotty, Henry Ledgard, Gregor von Bochmann · ACM Computing Surveys · 1976
From a purely scientific viewpoint, the members of the various working groups concerned with programming language standardization really ought to report to their parent committees that their assigned task is impossible without a major prior effort by the technical community; and that this prior effort would have to produce an effective procedure for describing the languages that are of concern.Thomas B. Steel, Jr., 1967 [$4] The current use of formal definitions of programming languages is very limited, largely because of a lack of fully developed techniques and because of user resistance to the poor human engineering of the definitions themselves.Nevertheless, usable formal definitions are essential for the effective design of programming languages and their orderly development and standardization.We present four well-known formal definition techniques: W-grammars, Production Systems with an axiomatic approach to semantics, the Vienna Definition Language, and Attribute Grammars.Each technique is described tutorially and examples are given; then each technique is applied to define the same small programming language.These definitions provide a usable basis for a critical discussion of the relative clarity of the different methods.This leads to a review of some of the debatable issues of formal definition.Among these issues are the advantages, if any, to the use of an underlying machine model, the precise nature of a valid program, the relative merits of generative and analytic definitions, and the place of implementationdefined features in the definition.Finally, a case is made for the importance of formal definitions and the need for a significant effort to make definitions suitable for human comprehension.