Nat; Clock generated by mkCIock; hour, minute total; This specification contains only syntactical functions for constructing a value of sort Clock (mkGIock) and for observing the syntactical information contained in such a representation (hour, minute).
3 1. Has each process a strong imperative verb and an object? 2. Are data flows in related to data flows out? Data should not be swallowed up by a process, only transformed in some way. ] 3. Can the flows be reduced? ] Six data flows in or out of a process should be sufficient. 4. Do all stores have flows both in and out? ]" [Eva92, p. ] In this style, several quality check and validation rules are given for the documents to be produced, some such rules also cover cross-document consistency checks.
Formal Foundations for Software Engineering Methods by Heinrich Hußmann (eds.)