Advantages of a Formal Specification of a Case From Informal Description via Formal Specification to Realization

Producing a complete, formal specification for an information system (IS) has several important advantages: Once we have a formal functional specification of an IS, the specification can serve as a solid starting point for several other development steps, such as generating default 'input forms', user stories, and default 'menus' per role. It also provides a potential means to prove (additional) state properties. Moreover, the specification can also serve as a 'quick reference guide' for the initiates working with the system. In this paper we are studying the practical suitability and appropriateness of the notion of information machine as means for formally specifying functional requirements. In this feasibility study we illustrate this by an example which is large and subtle enough to demonstrate how our approach works. It also shows the scalability and the ease of change. The specifications are implementation-independent (as it ought to be). Nevertheless we explain and illustrate how to generate a default implementation.