-
A specification is a written description of what a system is supposed to do.
-
Specifying a system helps us understand it.
-
Our basic tool for writing specifications is mathematics.
-
We define a behavior to be a sequence of states, where a state is an assignment of values to variables.
-
We specify a system by specifying a set of possible behaviors - the ones representing a correct execution of the system.
-
Temporal logic is a necessary evil.