A Hoare-like logic of asserted single-pass instruction sequences

DOI10.7561/SACS.2016.2.125zbMATH Open1424.68033arXiv1408.2955MaRDI QIDQ4621203FDOQ4621203

J. A. Bergstra, C. A. Middelburg

Publication date: 8 February 2019

Published in: Scientific Annals of Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1408.2955

Recommendations

• Hoare-style logic for unstructured programs
• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 3900131
• A compositional natural semantics and Hoare logic for low-level languages
• A compositional natural semantics and Hoare logic for low-level languages

zbMATH Keywords

completenessHoare logicsoundnessasserted single-pass instruction sequence

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

This page was built for publication: A Hoare-like logic of asserted single-pass instruction sequences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4621203)