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: |
|---|---|---|
| SortArray-class | package swt; public class SortArray extends java.lang.Object { swt.SortArray() { super(); } public static void swap(int i, int j, boolean[] reference_ar01) { boolean bv = reference_ar01[i]; reference_ar01[i] = reference_ar01[j]; reference_ar01[j] = bv; } public static void two_way_sort(boolean[] reference_ar01) { int i = 0; int j = reference_ar01.length - 1; while (i <= j) { if (! reference_ar01[i]) { i = i + 1; } else { if (reference_ar01[j]) { j = j - 1; } else { swt.SortArray.swap(i, j, reference_ar01); i = i + 1; j = j - 1; }}}} } | |
| Validref-axiom-init-SortArray | level⊆(`two-way-sort', str), validref(`two-way-sort', r, mkclasstype(`swt.SortArray' .class), st), validmode(`two-way-sort', st), st0 = st ⊦ [st; r0 = r.SortArray(); ] ( (st[_mode] = noval → validref(`two-way-sort', r0, mkclasstype(`swt.SortArray' .class), st)) ∧ validref(`two-way-sort', r, mkclasstype(`swt.SortArray' .class), st) ∧ valid⊆(str, st0, st) ∧ init⊆(str, st0, st) ∧ validmode(`two-way-sort', st)) | |
| Validref-axiom-init-swap | level⊆(`two-way-sort', str), validref(`two-way-sort', r, mkarraytype(boolean_type), st), validmode(`two-way-sort', st), st0 = st ⊦ [st; swt.SortArray.swap(i, i0, r); ] (validref(`two-way-sort', r, mkarraytype(boolean_type), st) ∧ valid⊆(str, st0, st) ∧ init⊆(str, st0, st) ∧ validmode(`two-way-sort', st)) | |
| Validref-axiom-init-two_way_sort | level⊆(`two-way-sort', str), validref(`two-way-sort', r, mkarraytype(boolean_type), st), validmode(`two-way-sort', st), st0 = st ⊦ [st; swt.SortArray.two_way_sort(r); ] (validref(`two-way-sort', r, mkarraytype(boolean_type), st) ∧ valid⊆(str, st0, st) ∧ init⊆(str, st0, st) ∧ validmode(`two-way-sort', st)) | |
| instfields-SortArray | ⊦ instfields(`swt.SortArray' .class) = [] | |
| statfields-SortArray | ⊦ statfields(`swt.SortArray' .class) = [] | |
| classex-two-way-sort | ⊦ class∃(`two-way-sort', class) ↔ class = `swt.SortArray' .class | |
| classex-two-way-sort-SortArray | ⊦ class∃(`two-way-sort', `swt.SortArray' .class) | |
| interfaceex-two-way-sort | ⊦ interface∃(`two-way-sort', class) ↔ false | |
| is_abstract-swtSortArrayclass-01 | ⊦ ¬ is_abstract(`swt.SortArray' .class) | |
| initdone-SortArray | ⊦ init(`two-way-sort', st) → initdone(`swt.SortArray' .class, st) | |
| ch-SortArray-ls | ⊦ `swt.SortArray' .class <_1 class ↔ class = `java.lang.Object' .class | |
| ch-SortArray-le | ⊦ `swt.SortArray' .class ≤ class ↔ ¬ ¬ (class = `swt.SortArray' .class ∨ `java.lang.Object' .class ≤ class) | |
| two-way-sort-corr-term | st[_mode] = noval, okarray(a, boolean_type, st), init(st), getbooleanarray(a, st) = bits ⊦ 〈st; swt.SortArray.two_way_sort(a); 〉 (issorted(getbooleanarray(a, st)) ∧ perm(getbooleanarray(a, st), bits) ∧ st[_mode] = noval) | A User Theorem |