THE TOY LANGUAGE SYNDROME
Original Publication Date: 1976-Jul-01
Included in the Prior Art Database: 2007-Mar-30
Software Patent Institute
Rosen, Barry K.: AUTHOR [+2]
Research Report RC 6083
Science 6 pages
THE TOY LANGUAGE SYNDROME
Barry K. Fasen
Computer Sciences Department I B M Thomas J. Watson Research Center Yorktown Heights, New York 10598 Typed by Marilyn Salvatore on MTST
San Jose . Yorktown - Zurich
(ij26285) 7 / 1 / 7 6 Computer
THE TOY LATTGUAGE SYNDROME
Barry K. Rosen
Computer Sciences Department
DM Thomas 3. Watson Research Center Yorktown Keights , New York 10598
Typed by Marilyn Salva.tore on MTST
ABSTRACT: Theorists and implementors can easily interact
in such a way that software performs improperly, even if there are no mathematical mistakes in the Geory and no codhg bugs in the implementation. This note explains the
problem and some ways to cope with it. Examples are drawn from program proving, language design, and code optimization. INDEX TERMS: Program verification, program proving, parallel progran, language design, call by name, call by value, side effects, code optimization, live variables, available expressions .
LIIIITED DISTRIBUTION NOTICE
This report has been submitted for publication elsewhere and has been issued as a Research Report for early dissemination of its contents. As a courtesy to the intended publisher, it should not be widely distributed until after the date of outside publication.
Copies may be requested from:
IBhl Thomas J. Watson Research Center Post Office Box 218
Yorktown Heights, New York 10598
1. AN ILLUSTRATIVE ERROR
A recent paper on proving properties of parallel programs contains a serious error that illustrates a fundamental difficulty in software engi- neerinq. After correctinq the error we w i l l consider therapeutic possibil- ities for the syndrome it illustrates. Lipton  claims to obtain condi- tions under which a proqram property need only be proved under the s i m ~ l i - wins assumption that a statement is "unintexruptible " or "indivisible. "
Statements here are as in "Algol or a similar language" 16, p. 7181 and can be nested witkin other statements.
If a statement S occurs in a program P, then the corresponding program w i t h S taken to be indivisible is denoted P/S and w i l l often behave differently .
Under certain conditions on S we miqht expect there to be no major difference.
i In particular, let S be any compound statement &g,& S1; S2; S3 &d such that S1 and S3 are dummy statements. The chanqe from P to P/S is a "D-reduction" according to the stated definition [6, P. 7201. Theorem 2 of [61 asserts that P halts iff PIS halts, where to "halt" is 1:o have at least one halting comput...