Author Archives

Research and Advances

Early experience with Mesa

The experiences of Mesa's first users—primarily its implementers—are discussed, and some implications for Mesa and similar programming languages are suggested. The specific topics addressed are: module structure and its use in defining abstractions, data-structuring facilities in Mesa, an equivalence algorithm for types and type coercions, the benefits of the type system and why it is breached occasionally, and the difficulty of making the treatment of variant records safe.
Research and Advances

Subgoal induction

A proof method, subgoal induction, is presented as an alternative or supplement to the commonly used inductive assertion method. Its major virtue is that it can often be used to prove a loop's correctness directly from its input-output specification without the use of an invariant. The relation between subgoal induction and other commonly used induction rules is explored and, in particular, it is shown that subgoal induction can be viewed as a specialized form of computation induction. A set of sufficient conditions are presented which guarantee that an input-output specification is strong enough for the induction step of a proof by subgoal induction to be valid.
Research and Advances

A bonus from van Wijngaarden’s device

In [1] van Wijngaarden presented a rather remarkable technique for rewriting ALGOL 60 programs to eliminate all labels. The purpose of this note is to point out that the rewriting would also eliminate the use of array returning (procedure returning, label returning, etc.) procedures had they been legal constructs of ALGOL 60. Hence, the many languages which allow such things to be returned as procedure values are not such large extensions of ALGOL 60 as one might think [2, 3, 4, 5].

Shape the Future of Computing

ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.

Get Involved