FORMAL DERIVATION TO OBJECT-ORIENTED IMPLEMENTATION OF FINANCIAL POLICIES

The use of formal methods promises correctness, verifiability, robustn ess and reliability of operational software systems which have been de veloped so far. Object-oriented methods enable easier development and maintenance of software application systems and promote the reuse of d esign and program code. Mapping formal specifications into an object-o riented application will therefore give a system that is not only corr ect and reliable, but easy to develop and enhance. In this paper, we s how how specifications containing major decisions that financial manag ers typically make, can be expressed in the Z notation. These specific ations are subsequently translated into pseudo object-oriented program s.