Towards Fully Abstract Semantics for Local Variables: Preliminary Report.

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 (lcps's), improved models and stronger proof rules are developed to handle such examples. Keywords: Languages, Semantics, Logic, Correctness, Block structure, Stack discipline, Functors.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1987
Accession Number
ADA191065

Entities

People

  • Albert R. Meyer
  • Kurt Sieber

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Weapons Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Availability
  • Calculus
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Information Processing
  • Information Systems
  • Language
  • Massachusetts
  • Military Research
  • Programming Languages
  • Reasoning
  • Security
  • Semantics
  • Standards

Fields of Study

  • Mathematics

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.