Operational semantics and generalized weakest preconditions (Q1330453)

Part of this paper was part of author's thesis (1991). It presents an operational semantics for the guarded command languages in which a computation is defined explicitly as a sequence of states through which execution of the program may evolve, starting from a certain initial state. The main contribution is a generalization of the Dijkstra's notion of weakest precondition. This generalization supports reasoning about general properties of programs, including temporal properties. Also, definition of the repetition was given in a closed form, which allowed the author to derive that repetition is equivalent to its first unfolding. Repetition has been defined both as the solution of a recursive equation and as the limit of its unfoldings. The author presents how to introduce the temporal property ``ever'' and the property ``leads-to''. By the so-called action systems a new theorem is proved.