The size and complexity of hardware and software systems
continues to grow,
making the introduction of subtle errors a more likely possibility.
A major goal of software engineering is
to enable developers to construct systems that operate reliably despite
increased size and complexity.
One approach to achieving this goal is through
formal methods: mathematically based languages, techniques and
tools for specifying and verifying complex software
systems.
In this paper, we apply a theoretical tool that is supported
by many formal methods, the correctness preserving
transformation (CPT), to a real software engineering
problem: the need for optimization during the maintenance
of code. We present four program transformations and a
model that forms a framework for proof of correctness.
We prove the transformations correct and
then apply them to a cryptography application.
Our experience shows that CPTs can facilitate generation
of more efficient code while guaranteeing
the preservation of original behavior.