Tutorial: Loop Invariant





The interactive transcript could not be loaded.


Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Sep 24, 2013

This video is part of a tutorial series for the Theorem Prover KeYmaera.

In this video we discuss how to apply a loop induction in KeYmaera.

First, we review the theory:

We want to prove that all runs of the hybrid program alpha* (which nondeterministically repeats alpha) will satisfy psi if and when they terminate.

This is essentially a poof by induction. We come up with a new property phi, called a loop invariant. We first prove that phi is satisfied initially. We then show that if phi holds, then it holds again after alpha executes. And finally, we prove that the loop invariant phi entails psi, the original property we wanted to prove.

Next we look at how to apply a loop induction rule in KeYmaera:

Option 1:
Drag and drop the file we want to prove into the tasks box, then click start. The top level operator in this hybrid program is a star, for nondeterministic repetition. By clicking on the box modality around the hybrid program, we see a list of possible operators, including the induction loop invariant rule. KeYmaera may try to guess the invariant and fill it in for you, but you can edit this formula, or paste in a new formula. You can also click on the alt tabs to view previously entered invariant choices.

Now that the rule has been applied, notice that the proof has split into three branches that must be closed before the property can be proved, just like the theoretical rule we introduced at the beginning. The Invariant is initially valid, which is the base case. The body preserves the invariant, which is the induction step. And the use case which checks that the invariant implies the original property we were trying to prove.

Option 1b:
Depending on your settings, KeYmaera may try to find a loop invariant and apply the induction rule automatically, in which case the prover may take a long time. If you get tired of waiting, you can stop KeYmaera, and inspect the loop invariant that was applied. To continue with the current loop invariant just click start. To change it, prune the proof before the invariant rule was applied, and then proceed as before.

Option 2:
So far we learned how to apply a loop invariant rule with user interactions in KeYmaera. However, the easiest way to apply a loop invariant is to directly annotate the .key file before loading it into keymaera. Edit the file so that immediately following the star, the annotation @invariant identifies the formula you want to use as a loop invariant. Then, when the file is loaded into keymaera, this rule will be applied without interaction.


When autoplay is enabled, a suggested video will automatically play next.

Up next

to add this to Watch Later

Add to

Loading playlists...