Animated, user friendly, formal specifications

Discusses PRECIS, a method for specifying sequential, non-concurrent systems based on a first order predicate logic. It operates by use of entities and the use of relationships between these entities. Since the method has a mathematical foundation, it is possible to reason logically about the properties of system specifications. It is also possible to test hypotheses and to attempt proofs to validate these hypotheses. The PRECIS method has a mathematical foundation and thus offers the possibilities of reasoning logically about the properties of specifications and proving theorems about the system being specified. Hence it satisfies the needs of safety critical systems in particular by allowing hypotheses to be put forward and tested.