It is apparent that some of the simplifications of Cook's ``toy'' language might be merely convenient to make the language and proof system smaller and more easily understandable; there would be no fundamental technical problems if these restrictions were relaxed. But others might be technically essential to obtain the results; they are imposed because, without them, the proof system would fail to be sound or relatively complete. As is often the case with such papers, Cook's discussion does not distinguish explicitly between these cases. His audience was mathematicians, not software engineers.
The ``meta-position'' of this position paper is that it is dangerous to err in either direction in characterizing these language simplifications as merely convenient or technically essential. Some software engineers tend to downplay the value of formal methods (especially in program verification) because they guess that nearly all the simplifications are essential; that the ``toy'' language is therefore so far removed from ``real'' ones that the results based on it can't possibly say anything interesting about the practical world. Others tend to guess that nearly all the simplifications are merely convenient; that the results for the ``toy'' language therefore apply to ``real'' ones that are similar. The only way to tell for sure (not just to guess) is to understand the proof system and the proof of its soundness and relative completeness; in other words, Cook's entire paper and then some. We have tried to do that, and to interpret two of our observations as specific positions to defend for this workshop:
Space limitations prevent us from defending these claims in any detail in this short position paper. Instead we note the relevance of the above claims to issues of software component reuse. We will, of course, be prepared to argue the validity of these positions at the workshop itself.
The first claim says that the full-fledged Ada and C++ languages permit legal programs (i.e., ones that compile without error) that may not submit to local certification of correctness. We cannot rely on the compiler to ``weed out'' the offending programs. If we want to be sure of the ability to reason modularly about programs — a prerequisite to successful component-oriented reuse [#!weide92!#] — then we must subscribe to a strict personal discipline or programming methodology such as that described by Hollingsworth for Ada [#!hollingsworth92!#]. Understanding which language simplifications are technically essential for modular reasoning tells us what guidelines this discipline must contain.
The second claim says that two of the restrictions in Cook's language that are most commonly considered to be technically essential are, in fact, not essential if one adopts a non-traditional parameter passing mechanism.
Ada includes a curiously indirect approach to these restrictions. An execution of a program whose effect depends on whether certain parameters are passed using call-by-reference or call-by-value-result is termed an ``erroneous execution.'' A call violating the repeated argument or global variable restriction almost certainly can distinguish between these mechanisms for some, but not necessarily all, values of its arguments. So defining dependence on the parameter passing mechanism as a source of erroneous execution is, in effect, a roundabout way of telling programmers not to violate the repeated argument and global variable restrictions. Note also that because array entries can be used as though they were variables, it is not always possible for an Ada compiler to detect violations of the repeated argument restriction. But an Ada compiler must accept a program as ``legal'' even when it is possible to determine at compile time that there is the potential for erroneous execution, because it is the execution that is defined to be erroneous, not the program.
On the basis of an admittedly superficial analysis, we conjecture that changing the explanation of parameter passing in Ada, from what is now in the language reference manual to call-by-swapping, would be an ``upward-compatible'' change in the following sense: (1) A legal Ada program that does not have the potential for erroneous execution under the current language definition would have the same effect if call-by-swapping were used. (2) A legal Ada program that does have the potential for erroneous execution due to dependence on the parameter passing mechanism under the current language definition would always give (modularly) predictable results if call-by-swapping were used. This change therefore could have important expressiveness consequences, especially in certain numerical and linear algebra applications where repeated arguments in procedure calls are both natural and desirable.