Formal Specification

Intro

• A specification is a statement of requirements for a system, object or process.
• A formal specification is one in which the language of mathematics is used to construct such a statement.
• Z is a formal specification language based on set theory and logic.
• In a Z specification, discrete mathematical structures are used to create a model of the required system.
• Predicate logic is used to state precisely the required relationships between the mathematical structures, thus defining the set of possible valid states for the system.
• The math structures are more abstract and problem oriented compared to the data structures used in programming languages.
• Predicate logic is then used to precisely define the required effect of operations in the system.
• Philosophy is to specify what each operation is supposed to do and not how to do it.

Proposition

• A proposition is a statement which is either true or false, but not both.
• e.g. 5 < 10 is a proposition, but not x > 0.