DocumentCode :
2597516
Title :
Axiomatizing operational equivalence in the presence of side effects
Author :
Mason, Ian A. ; Talcott, Carolyn
Author_Institution :
Lab. for Comput. Sci., Edinburgh Univ., UK
fYear :
1989
fDate :
5-8 Jun 1989
Firstpage :
284
Lastpage :
293
Abstract :
The authors present a formal system for deriving assertions about programs with side effects. The assertions considered are the following: (i) the expression e diverges (i.e. fails to reduce to a value); and (ii) e0 and e1 are strongly isomorphic (i.e. reduce to the same value and have the same effect on memory up to production of garbage). The e, ej are expressions of a first-order scheme- or Lisp-like language with the data operations atom, eq, car, cdr, cons, setcar, setcdr, the control primitives let and if, and recursive definition of function symbols
Keywords :
equivalence classes; formal languages; recursive functions; Lisp-like language; control primitives; data operations; if; let; memory model; operational equivalence; operational semantics; programs with side effects; recursive definition of function symbols; semantic consequence; strongly isomorphic; Abstracts; Calculus; Computer science; Contracts; Electrooptic effects; Production; Reasoning about programs; Tellurium;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
Conference_Location :
Pacific Grove, CA
Print_ISBN :
0-8186-1954-6
Type :
conf
DOI :
10.1109/LICS.1989.39183
Filename :
39183
Link To Document :
بازگشت