Go backward to A Model of Program Execution
Go up to Top
Go forward to Fundamental Concepts

Application of Execution Model

Fair selection condition:
- $R$ _i.label = $s$
  (for an infinite number of $i$ and any $R$ and $s$ ).
p[R_i]
- $p$ holds in $R$ _i.state.
{p} s {q}
- ( $p[R$ _i] and $R$ _i.label = $s$ ) $=>$ $q[R$ _i+1]
  (for all $R$ and $i$ ).

Program execution model used to formalize operational understanding of program execution, not to reason about program properties!

Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine