Specification and Animation of a Bank Transfer

DOI 10.1109/kbse.1995.490135 dblp

Abstract

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. It shows how animation may be helpful at several stages of a specification process based on a series of refinements of an initial abstract specification.

BibTeX

@inproceedings{Ledru:ASE95,
  author    = {Yves Ledru},
  title     = {Specification and Animation of a Bank Transfer},
  booktitle = {ASE},
  pages     = {192--199},
  publisher = {{IEEE} Computer Society},
  year      = {1995},
}

Specification and Animation of a Bank Transfer

Abstract

Related papers