Thumbnail
Access Restriction
Subscribed

Author Henderson, Peter
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword &lgr;-calculus ♦ Semantics ♦ Program correctness ♦ Formal description ♦ Programming languages
Abstract The constructs of a simple programming language are introduced and described informally in terms of values and side-effects. A translator is defined which translates the language into flowcharts for a simple machine. The action of the machine in executing a flowchart is defined. A proof is constructed that the effect of translating and executing any program can be expressed solely in terms of the value and side-effect of the program. During the course of constructing the proof, formal definitions of the concepts of value and side-effect are derived in order to make the proof rigorous. Correctness of the implementation involves checking that the definitions derived in the step above are an acceptable formalization of the informal description given in the first step.
Description Affiliation: Univ. of Newcastle upon Tyne, England (Henderson, Peter)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 15
Issue Number 11
Page Count 7
Starting Page 967
Ending Page 973


Open content in new tab

   Open content in new tab
Source: ACM Digital Library