Machine code and assembly language programs are structured using various branches and decision points, but between these they contain blocks of instructions that are simply sequentially composed. Most work on formal program analysis has focused on the behavior of the branch points — primarily because composing the blocks of sequential code to determine their overal effect on the system is often intellectually trivial. This processs is also computationaly simple, but it is not computationally trivial. The aim of this work is to produce a system of rules that can be efficiently implemented and allow us to determine the overal behaviour of sequentially composed operations. To identify those sequential compositions that are trivial we will use techniques inspired by Separation logic[2, 1]. Separation logic itself is a very general, abstract collection of higher order logic statements but the simple observation at the heart of separation logic will be used: if two operations refer to completely disjoint parts of the state space they can be reasoned about independently.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Taylor08,
author = {Ramsay Taylor},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {Separation of {Z} Operations},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {350},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_38},
doi = {10.1007/978-3-540-87603-8\_38},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/Taylor08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}