A Hoare-Like Logic of Asserted Single-Pass Instruction Sequences

Scientific Annals of Computer Science

article

J.A. Bergstra¹  C.A. Middelburg¹ 

[1] Informatics Institute, Faculty of Science, University of Amsterdam

关键词: Hoare logic;    asserted single-pass instruction sequence;    soundness;    completeness in the sense of Cook.;   

DOI  :  10.7561/SACS.2016.2.125

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

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.

【 授权许可】

CC BY-ND