Wp(S, R) represents the set of all states such that execution of S beginning in any one of them is guaranteed to terminate in a finite amount of time satisfying R.

• Wp(S, R) represents the set of all states such that execution of S beginning in any one of them is guaranteed to terminate in a finite amount of time satisfying R.

• Examples:

  • wp (i = i +1, i <= 1)
  • S: if x>=y then z = x else z = y, R: z = max(x,y)
    calculate wp(S,R)
  • Let S be as above and R: z=y, calculate wp(S,R)
  • S: if x>=y then z = x else z = y,R: z = y-1
    calculate wp(S,R)
  • Let S be as above, R: z= y+1

Previous slide

Next slide

Back to first slide

View graphic version