[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

A Rule for Loops

• An inference rule for logical pretest loops:

      {P} while B do S end {Q}
  

• The inference rule is:

  {I and B} S {I}

  {I} while B do S {I and (not B)}

• Where I is the loop invariant