A Hoare-like logic of asserted single-pass instruction sequences
Abstract
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.
Cite
@article{arxiv.1408.2955,
title = {A Hoare-like logic of asserted single-pass instruction sequences},
author = {J. A. Bergstra and C. A. Middelburg},
journal= {arXiv preprint arXiv:1408.2955},
year = {2017}
}
Comments
22 pages, the preliminaries have textual overlaps with the preliminaries in arXiv:1402.4950 [cs.LO] and earlier papers; introduction and conclusions rewritten, explanatory remarks added; introduction partly rewritten; 24 pages, clarifying examples added