Operational semantics and generalized weakest preconditions

AbstractDijkstra and Scholten (1990) present an axiomatic semantics for Dijkstra's guarded command language through the notions of weakest precondition and weakest liberal precondition. The informal notion of a computation is used as a justification for the various definitions. In this paper we present an operational semantics in which the notion of a computation is made explicit. The novel contribution is a generalization of the notion of weakest precondition. This generalization supports reasoning about general properties of programs (i.e. not just termination in a certain state) and we introduce two properties in this way