[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

A Harder Loop Invariant Example

    {P} while y < x + 1 do y := y + 1 {yɱ}
        {y > 5}y -> y + 1    => y > 4
        {y > 4}y -> y + 1    => y > 3

etc.

• Tells us nothing about x because x is not in Q = {y > 5}

• What else can we do?