Accession Number:

ADA191065

Title:

Towards Fully Abstract Semantics for Local Variables: Preliminary Report.

Descriptive Note:

Technical rept.,

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s):

Report Date:

1987-11-01

Pagination or Media Count:

19.0

Abstract:

The Store Model of Halpern-Meyer-Trakhtenbrot is shown--after suitable repair--to be fully abstract model for a limited fragment of ALGOL in which procedures do not take procedure parameters. A simple counter-example involving a parameter of program type shows that the model is not fully abstract in general. Previous proof systems for reasoning about procedures are typically sound for the HMT store model, so it follows that theorems about the counter-example are independent of such proof systems. Based on a generalization of standard cpo based models to structures called locally complete partial orders lcpss, improved models and stronger proof rules are developed to handle such examples. Keywords Languages, Semantics, Logic, Correctness, Block structure, Stack discipline, Functors.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE