A Logic for Expressions with Side Effects
Permanent Link(s)
Collections
Author
Boehm, Hans-J.
Abstract
This paper presents a simple programming logic LES, which is particularly well suited for reasoning about so-called expression languages, i.e. languages that incorporate imperative features into expressions rather than distinguishing between expressions and statements. An axiomatization of a simple programming language is presented using this formalism. It is shown that this axiomatization is relatively complete, roughly in the sense of [Coo 76].
Date Issued
1981-11
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-478
Type
technical report