Shared flowchart

Software · L5 · Proving a While Loop Correct

Sign in to clone

The three obligations a loop invariant must discharge, plus the extra variant obligation for total correctness.

by @openstemUpdated Software
Precondition P holds before the loopPropose loop invariant IInitialization: does P imply I?Preservation: does I and B, run through body C, re-establish I?Sufficiency: does I and not-B imply postcondition Q?Partial correctness established: P C QNeed total correctness too?Done: partial correctness sufficesFind variant: bounded-below expressionDoes variant strictly decrease every iteration?Total correctness established: loop always terminatesNoYesNoYesNoYesNoYesNoYes

We use privacy-friendly product analytics (no session recording, PII masked) to improve OpenStem. Load analytics? Privacy Policy