Property Preserving Development

This project will consider models of formal development of heterotic systems where the
computational properties are not necessarily preserved across steps.
Property Preserving Development. Formal development of systems proceeds stepwise,
where every step is motivated by a formal relation between the stages before and after that
step. This relation is normally expected to be the same, viz. "correctness preservation" at
every step. This is not entirely realistic, however: preservation of correctness is sometimes
too strong (e.g. replacing mathematical integers by machine ones), and sometimes too weak
(e.g. not enforcing improvements in executability or efficiency).
Heterotic Computing. 'Heterotic Computing' is defined as a combination of two or more
computational systems such that the combined system provides an advantage over either
individual substrate. These models have only been formalized recently, but in practice have
been ubiquitous for a while. Hybrid models have often been used to provide access to
properties and computational capacity for use in computational processes. It's a more recent
trend to try and formalize these systems, allowing them to extend their use past mere
convenience and into looking at when they can outperform single-paradigm systems.
One of the major challenges in developing heterotic systems is that data and functions are
modelled in a way that's natural to the specific substrate being used. The properties involved
in most current models are normally assumed to be preserved across substrates or any
areas of transduction. However, if the area is to be expanded (as many researcher fully
intend it to be) then it is imperative that models are created to ensure that changes in
properties are understood sufficiently to allow development.
The project will take aim to develop a formal framework of the relations between
computational abstractions and their representations across steps of refinement. The start of
the work will be based off Horsman e t al's work on Abstraction/Representation theory. Work
will start by developing an adaptation of AR theory that allows a stronger, more exact
definition of how abstractions are represented. This can then be looked at in conjunction with
model-driven refinement steps to create a framework of formal relations of how and where
correctness would not be preserved.