We write specifications of systems in order to be able to reason about those systems. This reasoning can be formal or informal. It can take the form of proving properties, deriving properties or refining the specification to code. The purpose of specifications is to allow this reasoning to take place, ie: specifications are for reasoning from. Looking at specification this way leads me to make the following suggestions:
- Specifications should be written in a way that makes reasoning easy. A way to do this is to write them as conjunctions of ready-to-use proof steps, with the pre-conditions and variables of each step clearly visible.
- Conciseness is not necessarily important in specifications. Not including irrelevant material is important, as is clearly laying out the relevant material, but using abstruse theories to make the specification as short as possible is not.
- Graphical notations that have not been designed with reasoning in mind should be avoided. Just because a notation is graphical does not mean that it makes reasoning easy.