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.
Preprint available:
arXiv:1408.2955 [cs.LO]