A Hoare-like logic of asserted single-pass instruction sequences
| Authors | |
|---|---|
| Publication date | 13-08-2014 |
| Number of pages | 21 |
| Publisher | Ithaca, NY: ArXiv |
| Organisations |
|
| 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. |
| Document type | Working paper |
| Note | Later versions also on arXiv.org |
| Language | English |
| Published at | http://arxiv.org/abs/1408.2955v1 |
| Downloads |
1408.2955v1.pd
(Submitted manuscript)
|
| Permalink to this page | |
