With some training, it must be possible to read and 'understand' specifications.
A specification must be minimal.
A specification technique should allow us to capture the 'correct' type of information in a natural way.
A formal method should provide a means for specifying a system so that consistency, completeness, and correctness can be assessed in a systematic fashion.
| Consistency | no contradictions (what is stated in one place is not contradicted in another). Consistency is ensured by mathematically proving that initial facts can be formally mapped into later statements within the specification. | |
| Completeness | difficult even for formal methods | |
| Correctness | could be achieved if there is a mapping between design and requirements. | |
| Precision | Lack of ambiguity | |
| Expressiveness | must be capable of expressing many different things as well as types of things (elements, objects, data, relationships, processes, properties ...)
Capable is not sufficient. To be expressive it must also allow for a convenient representation (that is in a straightforward way, does this mean perhaps natural?), and must support the other properties given below. |
| Semantic Soundness | has a mathematical foundation that allows correctness conditions to be stated |
| Programming Language Independent | |
| Machine Manipulability | use computer tools to manipulate the formalism |
| Combinability | methods for combining formal structures and assessing the properties of the whole from the properties of the parts. |
| Syntax | defines the specific notation with which the specification is represented. Typically the syntactic domain is based on standard set theory and predicate calculus. |
| Semantics | defines how representation describes a system requirements. Must be capable of expressing things that may not be computable. Furthermore these semantics must be capable of expressing system behavior. |
| Relations | the rules that indicate which objects properly satisfy the specification. |
| Expressiveness | Semantic Soundness | Independence | Manipulability | Combinab ility | |
| Natural Language | very capable of representing any kind or type of component. | Vague therefore not semantically sound (multitude of meanings possible) | yes | no | No theory to support combining text fragments |
| Programming Language | Not very limited in what it can represent (it can only represent computable functions) Useful for describing algorithmic behavior. | yes | no | yes | yes |
| Formal Grammar | Not Very | yes | yes | sort of | yes |
| Logical Formalism s | yes. can be used to represent many differing types of things (behavior, comp onents,...) but not very good at representing algorithmic processes | yes (within the expressive domain the meaning is exact) | yes | well? | yes. The theory generated by the union of two axioms systems is the union of the theories or a contradiction. |
| Informal | Expressed in natural language or pictures. |
| Specification by Pre- and Postconditions | {P} S {Q} We establish what should hold before, {P}, and after, {Q}, execution. We show that the program, S, transforms {P} to {Q}. As a design aid, this type of specification provides constraints which the implementation must satisfy.
Larch |
| Model Oriented | Provide a direct means to describe the system's behavior. The system is specified in terms of mathematical structures.
VDM and Z |
| Property Oriented | Use indirect means to specify behavior by stating the properties (constraints) the system must satisfy.
Eiffel, OBJ, AFFIRM |
Only highly critical systems benefit from their use
Formal methods involves complex mathematics
Formal methods increase the cost of development
Formal methods are incomprehensible to clients
Nobody uses formal methods for real projects