Separation of Z Operations

Introduction

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.