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

TL;DR

This paper introduces a Hoare-like logic framework for verifying the partial correctness of single-pass instruction sequences, accounting for jumps and multiple entry and exit points, enhancing understanding of low-level program correctness.

Contribution

It develops a formal system that extends traditional Hoare logic to handle the complexities of low-level instruction sequences with jumps and multiple control points.

Findings

Formal system for partial correctness proofs of instruction sequences

Handles multiple entry and exit points due to jumps

Supports sound reasoning about low-level programs

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.