Difference between revisions of "Formal Specification"
From Suhrid.net Wiki
Jump to navigationJump to searchLine 1: | Line 1: | ||
+ | = Intro = | ||
* A specification is a statement of requirements for a system, object or process. | * 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. | * A formal specification is one in which the language of mathematics is used to construct such a statement. | ||
Line 7: | Line 8: | ||
* Predicate logic is then used to precisely '''define the required effect of operations''' in the system. | * 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. | * Philosophy is to '''specify what''' each operation is supposed to do '''and not how''' to do it. | ||
+ | |||
+ | = Proposition = | ||
+ | |||
+ | |||
+ | = Predicate = |
Revision as of 10:02, 2 February 2012
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.