[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Finding Invariants (cont.)

• By extension, we get I = { y < x }

• When we factor in that the loop may not be executed even once (when y = x), we get

I = { y <= x }

• This also satisfies loop termination, so

• P = I = {y <= x}