Choice Semantics

Abstract

We now introduce a third semantic interpretation of statements, the choice semantics. Statements are here interpreted as functions that map each initial state to a set of predicates over the final state space. This means that we have altogether three different semantics for statements: an (operational) game semantics, a (backward) predicate transformer semantics, and a (forward) choice semantics. We show that these semantics are consistent with each other (we have already seen that this holds for the predicate transformer semantics and the game semantics). The predicate transformer semantics and the choice semantics are equivalent in the sense that either of them determines the other. The set of predicates that the choice semantics gives for an initial state is in fact the set of postconditions that the statement is guaranteed to establish from this initial state. Thus both choice semantics and predicate transformer semantics are abstractions of the game semantics in the sense that they can be determined from the game semantics for a statement. The converse does not hold, so the game semantics is more detailed than either of the other two. The choice semantics can be interpreted as describing a simple two-step game, so it is also directly connected to the view of statements as games.