ackerman

PVS‎ > ‎exercises‎ > ‎

Goal of exercise

Show that establishing program termination is not always straightforward: you need to specify an adequate measure and well founded relation, and then prove termination TCCs. In this case, in order to alleviate difficulties, we make use of an existing library, as an auxiliary tool providing the right well founded relation.

Underlying concept: recursive functions and well founded relations, PVS language handout pdf | ppt (slides 24--27).

Step by step

Create a new ackerman directory, e.g., ~login/pvs/ackerman/, and start PVS from this context.
Using Meta-x new-pvs-file command, create a new theory named ackerman;

Copy the ack definition of Ackerman function below:
ack(m, n: nat): RECURSIVE nat
= IF m = 0 THEN n+1
ELSIF n = 0 THEN ack(m-1, 1)
ELSE ack(m-1, ack(m, n-1))
ENDIF
MEASURE ???
BY ???
What measure? What well founded relation?

Lacking any precise idea, just pick identity as measure, and << as well founded relation, after declaring it as such just just before ack definition:
<<: (well_founded?[[nat, nat]]) ;
Launch type checking using Meta-x tc command and analyze proof obligations using Meta-x show-tccs to display them in a .TCCS buffer;
Try to prove all obligations automatically using Meta-x prove-pvs-file from ackerman theory buffer;
Refresh and display TCCS again using Meta-x show-tccs, and look at each TCC automatic proof using Meta-x show-proof with mouse pointer located within the TCC formula;
What remains to be proved? Is it possible?

Go back to previous question: choice of a well founded relation in [nat, nat]:

Try to discover a suitable well founded relation (allowing the proof of all termination TCCs): define << accordingly;
Do Meta-x pri to try to prove as much as possible automatically. What remains to be proved?

the answer is: there should be only one TCC left to be proved: << well foundedness.

What luck! There is a library about well founded relations developed at EIRBMMK:

~gloess/pvs/5.0/wf/5.0.wf.26oct2011.wf_properties.dmp.txt [with PVS proof status] for PVS 5.0;

Just

temporarily exit PVS ackerman context (you must quit PVS in order to avoid inconsistency problems);
create a wf directory at the same level as your ackerman directory (e.g., ~login/pvs/5.0/wf/);
copy the above dump into your wf directory;
start a new PVS session from this wf context;
restore wf library theories and proofs using Meta-x undump-pvs-files command;
prove everything in wf using Meta-x prove-importchain or Meta-x pri shortcut from wf_properties root theory buffer (which automatically triggers a type-check); check that everything (62 formulas) is proved complete like in original proof status;
you will need to import one and only one wf theory into from ackerman theory: which one? Look at wf_properties root theory for a list of wf theories, eventually check the theory you wish to import, using Ctrl c Ctrl f to load it;
imperatively quit this PVS session so as to guarantee consistency: your ackerman theory will use this wf library, and PVS must make sure you are not cheating by modifying wf while using it; if you do not quit, all your formulas relying upon wf library will be tagged "proved incomplete", as a punishment; it is OK, however, to open a simple Emacs session on wf context, in order to keep an eye on these theories;

Go back to ackerman context and start PVS from this context; import the theory you need (with appropriate instantiation of actuals) by adding these two lines before your definition of <<:

wf: LIBRARY = "../wf" ; % definition of wf library.
IMPORTING wf@???[?????] % import a specific theory instance to be determined.

Complete your proofs;

Remark: some students do not follow our advice, and manage to drive PVS into some incoherent state where it fears that the ackerman context has been developed upon an incomplete wf library context (and therefore refuses to consider all proofs complete): look at PVS at EIRBMMK > “What to do if your PVS context is no longer coherent”, to get around this situation!

DON'T IMMEDIATELY LOOK at solutions

~gloess/pvs/2.4/ackerman/2.4.ackerman.30oct2008.ackb.dmp.txt
~gloess/pvs/2.4/ackerman/2.4.ackerman.30oct2008.ackb.PVS_Status.txt

2007-2008 class: more pedagogical approach, in which the suitable definition of << is introduced before using wf library to prove its well foundedness;