De Montfort University
Suppose you have a computer program and you want to show that it works.
You could run it and see if you get the right answer.
But that only shows that it works for that particular input data.
There are a huge number of different values of input:
far to many to test all of them.
Instead of (or as well as) testing, you can use mathematical
logic to prove, or deduce, properties of the program.
Mathematics can prove things about an infinite set of data: for example,
we can prove that there are an infinite number of prime numbers.
Using mathematical logic we can prove that a program
is correct for ALL possible input data.
Mathematical logic has been around for centuries, but in the 1960's,
Carol Karp developed methods for extending logic so that you
can use infinitely long formulae. With this "infinitary logic"
we can write formulae about loops in programs: the formulae
are infinitely long, because we don't know exactly how many times
the program will go around the loop.
A "program transformation" is any operation on a program which
generates a new program which is equivalent to the original.
So the transformed program produces the same output as the original
program, when it is given the same input.
My research into program transformations started as a piece of pure
"blue skies" research with no commercial application. This research
turned out to have practical applications in reverse engineering:
this is analysing a program in a low-level language to determine
what it does and to translate it into a higher level language.
Many large organisations have systems running on mainframe computers:
which are very expensive to operate and maintain. My research
enables these companies to move some or all of their systems onto
more cost-effective PCs or workstations in a form which is much
easier to maintain.
A commercial company, Software Migrations Ltd, was set up to exploit
this research and now carries out migration projects involving millions
of lines of code.