Back to Search
Start Over
A Hoare-like logic of asserted single-pass instruction sequences
- Publication Year :
- 2014
- Publisher :
- arXiv.org, 2014.
-
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.
- Subjects :
- Computer Science::Hardware Architecture
Physics::Physics Education
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Accession number :
- edsair.narcis........d47a7c5e038a2ea3aa6e4480feb056a1