Browse Prior Art Database

THE TOY LANGUAGE SYNDROME

IP.com Disclosure Number: IPCOM000148562D
Original Publication Date: 1976-Jul-01
Included in the Prior Art Database: 2007-Mar-30

Publishing Venue

Software Patent Institute

Related People

Rosen, Barry K.: AUTHOR [+2]

Abstract

Research Report RC 6083 (11126285) 7/1/76 Computer Science 6 pages THE TOY LANGUAGE SYNDROMEBarry K. FasenComputer Sciences Department I B M Thomas J. Watson Research Center Yorktown Heights, New York 10598 Typed by Marilyn Salvatore on MTST Research Division San Jose . Yorktown Zurich RC 6083 (ij26285) 7 1 7 6 Computer Science THE TOY LATTGUAGE SYNDROME Barry K. RosenComputer 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 .

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 28% of the total text.

Page 1 of 10

Research Report

RC 6083

(11126285) 7/1/76
Computer

 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

Research Division


San Jose . Yorktown - Zurich

[This page contains 1 picture or other non-text object]

Page 2 of 10

[This page contains 1 picture or other non-text object]

Page 3 of 10

RC 6083

(ij26285) 7 / 1 / 7 6 Computer

Science

6 pages

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 .

[This page contains 1 picture or other non-text object]

Page 4 of 10

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

[This page contains 1 picture or other non-text object]

Page 5 of 10

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 [6] 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...