[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Finding Loop Invariants

• Work backwards through a few iterations and look for a pattern

      while y <> x do y:= y+1   {y = x}
  
       {P?}  y := y + 1  {y = x}
       P = {y = x}y -> y + 1 = {y = x-1}    --last iteration
       {P?}  y := y + 1  {y = x-1}
       P = {y = x-1}y -> y + 1 = {y = x-2}    --next to last