This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| ArrayMax-class | package swt; public class ArrayMax extends java.lang.Object { swt.ArrayMax() { super(); } public static int max(int[] a) { int i = 0; int i0 = a.length - 1; while (i != i0) { if (a[i] <= a[i0]) i++; else i0--; }return i; } } | |
| Validref-axiom-init-ArrayMax | level⊆(`Challenge1', str), validref(`Challenge1', r, mkclasstype(`swt.ArrayMax' .class), st), validmode(`Challenge1', st), st0 = st ⊦ [st; r0 = r.ArrayMax(); ] ( (st[_mode] = noval → validref(`Challenge1', r0, mkclasstype(`swt.ArrayMax' .class), st)) ∧ validref(`Challenge1', r, mkclasstype(`swt.ArrayMax' .class), st) ∧ valid⊆(str, st0, st) ∧ init⊆(str, st0, st) ∧ validmode(`Challenge1', st)) | |
| Validref-axiom-init-max | level⊆(`Challenge1', str), validref(`Challenge1', r, mkarraytype(int_type), st), validmode(`Challenge1', st), st0 = st ⊦ [st; i = swt.ArrayMax.max(r); ] (validref(`Challenge1', r, mkarraytype(int_type), st) ∧ valid⊆(str, st0, st) ∧ init⊆(str, st0, st) ∧ validmode(`Challenge1', st)) | |
| instfields-ArrayMax | ⊦ instfields(`swt.ArrayMax' .class) = [] | |
| statfields-ArrayMax | ⊦ statfields(`swt.ArrayMax' .class) = [] | |
| classex-Challenge1 | ⊦ class∃(`Challenge1', class) ↔ class = `swt.ArrayMax' .class | |
| classex-Challenge1-ArrayMax | ⊦ class∃(`Challenge1', `swt.ArrayMax' .class) | |
| interfaceex-Challenge1 | ⊦ interface∃(`Challenge1', class) ↔ false | |
| is_abstract-swtArrayMaxclass | ⊦ ¬ is_abstract(`swt.ArrayMax' .class) | |
| initdone-ArrayMax | ⊦ init(`Challenge1', st) → initdone(`swt.ArrayMax' .class, st) | |
| ch-ArrayMax-ls | ⊦ `swt.ArrayMax' .class <_1 class ↔ class = `java.lang.Object' .class | |
| ch-ArrayMax-le | ⊦ `swt.ArrayMax' .class ≤ class ↔ ¬ ¬ (class = `swt.ArrayMax' .class ∨ `java.lang.Object' .class ≤ class) | |
| arrayMaxWhile | st[_mode] = noval, okarray(a, int_type, st), init(st), getintarray(a, st) ≠ [] ⊦ 〈st; i = swt.ArrayMax.max(a); 〉 (st[a -- i '] .intval = max(getintarray(a, st)) ∧ 0 ≤ i ∧ i < st[a -- _length] .intval) | A User Theorem |