Tobsan

//Invariant: (p.size + 1) == size{p.header.*next} && ...public class LinkedList {   Entry header;   int size;   class Entry {     Entry next;     Object element;     Entry/Entry n, Object e) { next = n; element = e; }   }//Returns the removed objectObject remove(int index) { ... }public LinkedList tail() {   LinkedList tl = new LinkedList();   tl.header.next = this.header.next.next;   tl.size = this.size -1;   return tl;   }}