package dataStructures;

import java.util.*;

/**
 * <p>Titulo: A interface do TDA Lista</p>
 * <p>Descrição: O desenho da Lista (List) com os respectivos contratos</p>
 * @version 1.0
 */

public interface List {

  //@ public invariant !isEmpty() ==> head() != null;

  /**
   * Criar uma lista vazia
   * @return uma lista vazia
   */

  //@ ensures \result.isEmpty();
  /*@ pure @*/ List empty();

  /**
   * A lista está vazia?
   * @return TRUE se está vazia, FALSE c.c.
   */
  /*@ pure @*/ boolean isEmpty();

  /**
   * Adicionar à lista um novo objecto
   * @param o a referência do objecto a adicionar
   */

  //@ requires o != null;
  //@ ensures head().equals(o);
  //@ ensures tail().equals((List)\old(clone()));
  void cons(Object o);

  /**
   * Devolver o elemento que está no inicio da fila
   * @return a referência do primeiro elemento
   */

  //@ requires  !isEmpty();
  /*@ pure @*/ Object head();

  /**
   * Devolver o resto da lista
   * @return a referência para o resto da lista
   */

   //@ requires !isEmpty();
   /*@ pure @*/ List tail();

  /**
   * Calcular o número de elementos da lista
   * @return o número de elementos da lista
   */

  //@ ensures  isEmpty() ==> \result == 0;
  //@ ensures !isEmpty() ==> \result == 1 + tail().length();
  /*@ pure @*/ int length();

  /**
   * Descobrir o n-ésimo elemento da lista
   * @param n a posição requerida
   * @return a referência para o n-ésimo elemento
   */

  //@ requires n > 0 && length() >= n;
  //@ ensures n==1 ==> \result.equals(head());
  //@ ensures n!=1 ==> \result.equals(tail().get(n-1));
  /*@ pure @*/ Object get(int n);

  /**
   * Inserir no início
   * @param o a referência do elemento a ser inserido
   */

  //@ requires  o != null;
  //@ ensures head().equals(o);
  //@ ensures tail().equals((List)\old(clone()));
  void addBegin(Object o);

  /**
   * Inserir no fim
   * @param o a referência do elemento a ser inserido
   */

  //@ requires  o != null;
  //@ ensures length() == \old(length()) + 1;
  //@ ensures get(length()).equals(o);
  //@ ensures (\forall int i; 1 <= i && i <= length()-1; ((List)\old(clone())).get(i).equals(get(i)));
  void addEnd(Object o);

  /**
   * Inserir na n-ésima posição
   * @param o a referência do elemento a ser inserido
   * @param n a posição de inserção (n=1 insere no início)
   */

  //@ requires  o != null;
  //@ requires  n > 0 &&  n <= length();
  //@ ensures length() == \old(length()) + 1;
  //@ ensures get(n).equals(o);
  //@ ensures (\forall int i; n <= i && i <= \old(length()); ((List)\old(clone())).get(i).equals(get(i+1)));
  //@ ensures (\forall int j; 1 <= j && j <= (n-1); ((List)\old(clone())).get(j).equals(get(j)));
  void add(Object o, int n);

  /**
   * Remover o primeiro elemento
   */

  //@ requires !isEmpty();
  //@ ensures equals(((List)\old(clone())).tail());
  void removeBegin();

  /**
   * Remover o último elemento
   */

  //@ requires !isEmpty();
  //@ ensures length() == \old(length()) - 1;
  //@ ensures (\forall int i; 1 <= i && i <= length()-1; ((List)\old(clone())).get(i).equals(get(i)));
  void removeEnd();

  /**
   * O objecto está na lista?
   * @param o a referência do elemento a ser procurado
   * @return TRUE se o objecto existe, FALSE c.c.
   */

  //@ ensures \result == (!isEmpty() && (o.equals(head()) || tail().contains(o)));
  /*@ pure @*/ boolean contains(Object o);

  /**
   * Devolver a posição da primeira referência do objecto na lista, se
     o objecto não existir, devolve zero.
   * @param o a referência do objecto a procurar
   * @return a posição do 1º objecto igual a 'o', senão Zero
   */

  //@ requires o != null;
  //@ ensures !contains(o) ==> \result == 0;
  //@ ensures  contains(o) &&   o.equals(head())  ==> \result == 1;
  //@ ensures  contains(o) && !(o.equals(head())) ==> \result == 1 + tail().indexOf(o);
  /*@ pure @*/ int indexOf(Object o);

  /**
   * Remover a 1ª ocorrência de um elemento
   * @param o a referência do elemento que serve de comparação para a remoção
   */

  //@ requires o != null;
  //@ ensures \old(contains(o)) ==> length() == \old(length()) - 1;
  void remFirst(Object o);

  /**
   * Remover todas as ocorrências de um elemento
   * @param o a referência do elemento que serve de comparação para a remoção
   */

  //@ requires o != null;
  //@ ensures !contains(o);
  void remAll(Object o);

  /**
   * Concatenar duas listas
   * @param l a lista a ser concatenada no fim desta lista
   */

  //@ requires l != null;
  //@ ensures length() == \old(length()) + l.length();
  //@ ensures (\forall int i; 1 <= i && i <= \old(length()); ((List)\old(clone())).get(i).equals(get(i)));
  //@ ensures (\forall int j; \old(length()) < j && j <= length(); get(j).equals(l.get(j-(\old(length())))));
  void concat(List l);

  /**
   * Inverter a lista
   */

  //@ ensures length() == \old(length());
  //@ ensures (\forall int i; 1 <= i && i <= length(); ((List)\old(clone())).get(i).equals(get(length()-i+1)));
  void reverse();

  /**
   * Sao as duas listas iguais?
   * @param l a lista a ser comparada
   * @return TRUE se this==o, FALSE c.c
   */

  //@ requires l != null;

  //@ ensures isEmpty() ==> \result == l.isEmpty();
  //@ ensures !isEmpty() ==> \result == (!(l.isEmpty()) && head().equals(l.head()) && tail().equals(l.tail()));
  /*@ pure @*/ boolean equals(List l);

  /**
   * Devolver uma cópia da estrutura.
   * @return uma referencia para a cópia
   */

  //@ also
  //@ ensures (\result != this) && equals((List)\result);
  /*@ pure @*/ Object clone();

}//endInterface List