Ordinal Numbers

Download or Start

KeY requires Java version 8 or newer and is tested on Linux, OS X and Microsoft Windows.

• Instant Start: Web Start
• Binary Version: KeY
• Source Code: KeY-src.zip
• GoodsteinBig.java This program computes Goodstein sequences using Java’s BigInteger class. This program is not mentioned in the paper.
• Goodstein.java The file “Goodstein.java” contains the Java program that is analysed in the paper. It does not correctly compute Goodstein sequences once they grow beyond maxInt. But, since in the default setting KeY treats Java integers as mathematical integer the performed analysis is correct.
  In the paper the JML annotations of “Goodstein.java” have been reduced to the essential core. Here the full annotation is shown. Also the auxiliary method for computing exponentials “intPow” is included
• Program Correctness Proofs This tarfile contains the proofs of the contracts of the three methods in “Goodstein.java”. Proof files can be loaded in the KeY system the same way as annotated Java programs: in the pull-down menue “file” choose “load” and select the wanted proof file. After loading you may inspect the finished proof. To keep things simple the unpacked proof files should be placed in the same directory as Goodstein.java.
• The technical report contains more material than could be covered in the page resticted paper.
• The program correctness proofs use a number of lemmas on ordinals, the embedding of positive integers into ordinals, and termination functions introduced for Goodstein sequences. Proofs of these lemmas are contained in the zip-files OrdProofs1 OrdProofs2 OrdProofs3 respectively. The files in these zip-archives use KeY internal names. The correspondence between the lemma whose proof you want to inspect and the name of the proof file can be retrieved from Fml2Taclet. To inspect the proofs, start the KeY system and select in the pull-down menue “file” subitem “load” the wanted proof file. Proof files come with extensions .key or .proof. The user will not note any difference after loading them. The .proof files contain saved finished proofs. The .key files contain commands of a simple, experimental scripting language that construct the proof on the fly. In some rare cases the proof in a .key file does not complete. It has to be completed manually, which is in all cases trivial if you know how to handle the prover. This phenomenon is due to deficiencies of the scripting language.

[button type=”primary” size=”lg” link=”http://formal.iti.kit.edu/key/tableaux17/webstart/KeY.jnlp”][icon type=”play”] Run KeY via Webstart [/button]