Operational semantics and generalized weakest preconditions (Q1330453)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Operational semantics and generalized weakest preconditions |
scientific article |
Statements
Operational semantics and generalized weakest preconditions (English)
0 references
21 July 1994
0 references
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.
0 references
operational semantics
0 references
weakest precondition
0 references
unfolding
0 references
temporal property
0 references