I need your help with the specification construction tool again.
The tool is at:
http://webfea.fea.aub.edu.lb/fadi/dkwk/doku.php?id=speccheck

I need you to help us with using the specification construction tool to build the following given what we have built before:

1. binary search "int binary search(a, left, right, e)"
        precondition (array is ordered, left valid, right valid)
        postcondition (array is ordered, left valid, right valid, the return value is the index of e in a, or -1 if e is not in a)

        assume you have eina, isvalid, linear-search(a,left,right,e) as predicates that you have already built and use them in the theory files as boolean variables and vocabulary clauses.

2. Linked list:
    isnodeconsistent(next[], prev[], i, n, p)   
    express whether the pointed to by i is consistent or not where next and prev designate arrays of next and prev pointers and where -1 is an invalid addrees. You may use n and p as auxiliary variables with clauses (n=next[i]) and (p=prev[i]) to have the smt solver relax when passing queries to it.

3. Binary heap:
      isvalid(a[], i) expression that returns whether i is a valid index of  array  a

      isleft(a[],i,left) check whether left is the left child of element at index i in the binary heap represent by array i, a valid left child is at index 2*i+1 when i is valid. Use isvalid also as a predicate.

      isright(a[],i,right) check whether right is the right child of element at index i in the binary heap represent by array i, a valid right child is at index 2*i+1 when i is valid. Use isvalid also as a predicate.

      isnotheap(a[]) checks whether array a represents a heap or not. You may need to use two auxiliary variables (i and j) and the predicates you defined so far as well in your vocab/theory.

4. array implementation of a root indexed tree. check the double array trie paper/website http://linux.thai.net/~thep/datrie/
 try to read about it and come up with expressions you want to express (in english) and use the tool to express.

I highly appreciate it if you can return to me as soon as possible with the following:

1. the theory files
2. the session files