Correctness of the compiling process based on axiomatic semantics

descriptionPublicationkeyboard_double_arrow_right Article 01 Jun 1980 English Publisher:Springer Science and Business Media LLCJournal:Acta Informatica, volume 14, pages 1-20 (issn: 0001-5903, eissn: 1432-0525,

Copyright policy )

Authors: Bruce Russell;

doi: 10.1007/bf00289061

Correctness of the compiling process based on axiomatic semantics

- Summary
- Subjects
- Metrics

Abstract

A language that includes computed gotos and parameterized procedures is defined and its semantics are given axiomatically. A number of program transformations are described and proved correct. Taken collectively and applied repeatedly these transformations compile the full language into a low level subset.

Related Organizations

Stony Brook University
United States

Keywords

block structured programming language, Specification and verification (program logics, model checking, etc.), correctness, axiomatic semantics, program transformations, verification rules, General topics in the theory of software

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	2
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average