Formal derivation to object-oriented implementation of financial policies

Abstract

The use of formal methods promises correctness, verifiability, robustness and reliability of operational software systems which have been developed so far. Object-oriented methods enable easier development and maintenance of software application systems and promote the reuse of design and program code. Mapping formal specifications into an object-oriented application will therefore give a system that is not only correct and reliable, but easy to develop and enhance. In this paper, we show how specifications containing major decisions that financial managers typically make, can be expressed in the Z notation. These specifications are subsequently translated into pseudo object-oriented programs.