package java.lang;

import java.util.*;

/*@

inductive unit = unit;

inductive pair<a, b> = pair(a, b);

fixpoint a fst<a, b>(pair<a, b> p) {
    switch (p) {
        case pair(x, y): return x;
    }
}

fixpoint b snd<a, b>(pair<a, b> p) {
    switch (p) {
        case pair(x, y): return y;
    }
}

fixpoint t default_value<t>();

inductive boxed_int = boxed_int(int);
fixpoint int unboxed_int(boxed_int i) { switch (i) { case boxed_int(value): return value; } }

inductive boxed_bool = boxed_bool(boolean);
fixpoint boolean unboxed_bool(boxed_bool b) { switch (b) { case boxed_bool(value): return value; } }

predicate array_element<T>(T[] array, int index; T value);
predicate array_slice<T>(T[] array, int start, int end; list<T> elements);
predicate array_slice_deep<T, A, V>(T[] array, int start, int end, predicate(A, T; V) p, A info; list<T> elements, list<V> values);

lemma_auto void array_element_inv<T>();
    requires [?f]array_element<T>(?array, ?index, ?value);
    ensures [f]array_element<T>(array, index, value) &*& array != null &*& 0 <= index &*& index < array.length;

lemma_auto void array_slice_inv<T>();
    requires [?f]array_slice<T>(?array, ?start, ?end, ?elems);
    ensures [f]array_slice<T>(array, start, end, elems) &*& array != null &*& 0 <= start &*& start <= end &*& end <= array.length &*& start + length(elems) == end;

lemma_auto void array_slice_deep_inv<T, A, V>();
    requires [?f]array_slice_deep<T, A, V>(?array, ?start, ?end, ?p, ?info, ?elems, ?vs);
    ensures [f]array_slice_deep<T, A, V>(array, start, end, p, info, elems, vs) &*& array != null &*& 0 <= start &*& start <= end &*& end <= array.length &*& start + length(elems) == end;

lemma void array_slice_deep_close<T, A, V>(T[] array, int start, predicate(A, T; V) p, A a);
    requires array_slice<T>(array, start, start + 1, ?elems) &*& p(a, head(elems), ?v);
    ensures array_slice_deep<T, A, V>(array, start, start + 1, p, a, elems, cons(v, nil));

lemma void array_slice_deep_open<T, A, V>(T[] array, int start);
    requires array_slice_deep<T, A, V>(array, start, start + 1, ?p, ?a, ?elems, ?vs);
    ensures array_slice<T>(array, start, start + 1, elems) &*& p(a, head(elems), head(vs));

lemma void array_slice_split<T>(T[] array, int start, int start1);
    requires array_slice<T>(array, start, ?end, ?elems) &*& start <= start1 &*& start1 <= end;
    ensures
        array_slice<T>(array, start, start1, take(start1 - start, elems)) &*&
        array_slice<T>(array, start1, end, drop(start1 - start, elems)) &*&
        elems == append(take(start1 - start, elems), drop(start1 - start, elems));

lemma void array_slice_join<T>(T[] array, int start);
    requires
        array_slice<T>(array, start, ?start1, ?elems1) &*& array_slice<T>(array, start1, ?end, ?elems2);
    ensures array_slice<T>(array, start, end, append(elems1, elems2));

lemma void array_slice_deep_split<T, A, V>(T[] array, int start, int start1);
    requires array_slice_deep<T, A, V>(array, start, ?end, ?p, ?a, ?elems, ?vs) &*& start <= start1 &*& start1 <= end;
    ensures
        array_slice_deep<T, A, V>(array, start, start1, p, a, take(start1 - start, elems), take(start1 - start, vs)) &*&
        array_slice_deep<T, A, V>(array, start1, end, p, a, drop(start1 - start, elems), drop(start1 - start, vs));

lemma void array_slice_deep_join<T, A, V>(T[] array, int start);
    requires
        array_slice_deep<T, A, V>(array, start, ?start1, ?p, ?a, ?elems1, ?vs1) &*&
        array_slice_deep<T, A, V>(array, start1, ?end, p, a, ?elems2, ?vs2);
    ensures array_slice_deep<T, A, V>(array, start, end, p, a, append(elems1, elems2), append(vs1, vs2));

lemma void array_slice_deep_empty_close<T, A, V>(T[] array, int start, predicate(A, T; V) p, A a);
    requires array != null &*& 0 <= start &*& start <= array.length;
    ensures array_slice_deep<T, A, V>(array, start, start, p, a, nil, nil);

@*/

public class Object {

    public Object();
        //@ requires emp;
        //@ ensures emp;

}

public class InterruptedException {}

public class IOException {}

public class RuntimeException {

    public RuntimeException();
        //@ requires true;
        //@ ensures true;

    public RuntimeException(Object innerException);
        //@ requires true;
        //@ ensures true;

}

public class Integer {

    public static final int MAX_VALUE = 0x7fffffff;
    public static final int MIN_VALUE = -0x80000000;
    
    public static int parseInt(String s);
    	//@ requires s != null;
        //@ ensures true;
    

}