# States and Semantics

### States

**State space**: In this book, the **state space** is regarded as being built up as a **Cartesian product**, and the states is the points.

**Predicate** is the formal expression of **condition**. Each predicate is assumed to be defined in each point of the state space. Given a point, the value of a predicate is either “True” or “False”. Therefore, the predicate characterize the set of all points where the predicate is true. Two predicates `P = Q`

, when they characterize the same set of states.

`T`

is the predicate that is true in all points of the state space. `F`

is the predicate that is false in all points of the state space.

### Semantics

**Deterministic machines**: the happening that will take place upon activation of the mechanism is fully determined by its initial state.

**Nondeterministic machines**: activation in a given initial state will give rise to one out of a class of possible happenings, the initial state only fixing the class as a whole.

**Post-condition**: In computer programming, a post-condition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. via wiki

**Weakest pre-condition corresponding to that post-condition**: the condition that characterizes the set of all initial states such that activation will certainly result in a properly terminating happening leaving the system in a final state satisfying a given post-condition. If the system is denoted by `S`

and the desired post-condition by `R`

, then we denote the corresponding weakest pre-condition by `wp(S, R)`

**A predicate transformer**: For a fixed mechanism `S`

such a rule, which is fed with the post-condition `R`

and delivers the corresponding weakest pre-condition `wp(S, R)`

, is called “a predicate transformer”.

**Sufficient pre-condition**: `P`

is a sufficient pre-condition, denoted as `P => wp(S, R)`

, requires that wherever `P`

is true, `wp(S, R)`

is true as well.