Specification and Animation of a Bank Transfer using KIDS/VDM

摘要

The development of formal specifications may benefit from prototyping activities. The production of an executable model for a given description helps bridging the gap between this specification and the corresponding reality. The KIDS/VDM system, based on the KIDS environment, provides these prototyping facilities for the model-based specification language of VDM. This paper illustrates its use in the specification of a bank transfer operation. The specification process starts from an abstract specification and details it by a series of refinements of either the control flow or the data structures. The case study shows how animation may be helpful at several stages of the process. It favours the dialog between the specifier and his customer and helps assessing the correspondence between the description and the actual problem. It also convinces the specifier of the validity of his refinements before he fulfills the necessary proof obligations.