Effects systems statically calculate the state affected or required by an execution. The effect is given in terms of some abstraction of the state of the program. The effect of an expression is given in two parts - the state which is read and that which is written to. The effect of two expressions can show them to be non-interfering and thus can be used to choose when to parallelise code. Similarly, effects can indicate when it is safe to re-order code whilst preserving the semantics.
We extend the calculation of effects to predicates and show how it is possible to calculate the effect of a predicate (the part of the program state required to calculate satisfaction). We then extend the definition of non-interference for predicates and expressions (where the execution does not affect satisfaction of the predicate). This property can be derived statically using effects and we suggest an application in verification. We have developed a language independent model of effects. Our model is able to describe complex and abstract properties of such systems without reference to particular language features. The model includes predicates and their effects. Results proved within our model show that any language and effects system which fits the model can judge noninterference properties.
We define ODE, an effects system for Ownership Domains. Ownership Domains are an extension of Ownership Types and provide finer granularity of encapsulation but also a more liberal aliasing policy. We base our effects system on that of Joe. The increased precision of Ownership Domains allows us to provide more precise effects than would be possible in Joe. We prove that ODE is an instance of our model of effects.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.