Go backward to Leads-to
Go up to Top
Go forward to An Example
Fixed Point
- Fixed Point = program state
- Execution of any statement in that state leaves state unchanged.
- Once reached, program remains in this state.
- Equivalent to termination in sequential programming.
- Predicate FP for program G:
- FP <forall : in and is X
:= :: = >.
- Program execution model:
- FP[] <forall : ::
.state = .state>
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine