Structuring control in Fortran
A. E. Sedgwick · ACM SIGPLAN Notices · 1977
This note suggests yet another view as to what compound statements should be introduced into languages such as Fortran.In this proposal, selection and refinement are the key constructs and a radically simple approach to repetition due to Hehner [1976] is presented .A major goal in defining the control constructs is to keep the semantics as simple as possible .We would like to encourage the programmer to invent informal or formal assertions describing the state of the computation at various points in the program.The assertions reduce the dynamic relationship between variables and values to invariant expressions .Unfortunately, many existing control con-st~ructs have sufficiently complicated semantics to discourage the programmer from thinking this way .The semantics of the statement S determine for any predicate R the weakest precondition such that the execution of S will establish R.This weakest precondition might be denoted S : R following the suggestion of Hehner [1976] .Then the semantics of executing S1 followed by S2 might be denoted (S1 S2) : R = S1 : (S2 : R) = S1 : S2 : R .That this composition seems so trivial is a credit to the notation .Of course, the weakest precondition X = E : R, for the assignment X = E to establish R, would be R with all free occurrences of X in R replaced by the expression E .(Note that the notation Ri is not very convenient when composition is considered .The unabbreviated notation X = E .R is more convenient .)Dijkstra [1976] gives many examples of the "calculus" of preconditions .With this point of view for semantics we now introduce the' control constructs .The syntax is informal with lower-case letters for non-terminals, and is just a suggestion .The only new character is the double-quote symbol which is available in all modern character sets .(If necessary, it could be replaced,by another character as in Hull [1976] .)The predicates pi are logical expressions.The semicolon is used in' some of=the examples as a -statement separator merely to compress the examples .