package gestionProc;

import java.util.List;

/** Repr'esentation d'une liste contenant des processus non nuls.<br> 
  Une telle liste ne contient pas deux processus de meme identifiant. <br>
  Il est possible :
  <ul>
  <li>de d'eterminer si un processus d'identifiant donn'e appartient `a cette liste;</li>
  <li>d'ajouter un processus `a la liste (sans pr'eciser o`u se fait l'insertion);</li>
  <li>de retirer un processus de la liste (sans pr'eciser lequel).</li>
  </ul>
 * @author M. Nebut
 * @version 02/05
 */
public interface ProcessusList {

    /** Invariant de classe */
    /*@ public invariant plist != null; @*/

    /*@ public model instance List plist; @*/

    /** Retourne vrai si cette liste de processus est vide.
     * @return vrai si le nombre d''el'ements de cette liste vaut 0
     */
    /*@
      @ ensures \result <==> plist.isEmpty();
      @*/
    public /*@ pure @*/ boolean empty();

    /** Retourne le nombre d''el'ements de cette liste de processus.
     * @return le nombre d''el'ements de cette liste
     */
    /*@
      @ ensures \result == plist.size();
      @*/
    public /*@ pure @*/ int nbElem();

    /** Ajoute le processus <tt>p</tt> dans cette liste de
     * processus. M'ethode non-d'eterministe : l'emplacement de
     * l'insertion n'est pas pr'ecis'e. 
     * @param p un processus `a ajouter `a la liste
     */
    /*@
      @ requires p != null;
      @ requires ! plist.contains(p);
      @
      @ assignable plist;
      @
      @ ensures \old(plist.size()) == plist.size() - 1; // La taille a augmenté d'un
      @ ensures (\forall int i; i >= 0 && i < \old(plist.size()); plist.contains(\old(plist.get(i)))); // Pas de modifications dans la liste
      @ ensures plist.contains(p); // L'élément a bien été ajouté
      @*/
    public void ajouterProcessus(Processus p);

    /** Retire un processus de cette liste et le retourne. M'ethode
     * non-d'eterministe : ne pr'ecise pas quel processus est retir'e.
     * @return un processus de la liste 
     */
    /*@ requires ! empty();
      @ assignable plist;
      @
      @ ensures \old(plist.size()) == plist.size() + 1; // La taille a diminué d'un
      @ ensures (\forall int i; i >= 0 && i < \old(plist.size()); \old(plist.get(i)).equals(\result) || plist.contains(\old(plist.get(i)))); // La liste n'a pas changé
      @ ensures ! plist.contains(\result); // On n'a plus l'élément retourné
      @*/
    public Processus retirerProcessus();

    /** Retourne vrai si cette liste contient le processus <tt>p</tt>.
     * @param p le processus dont on souhaite tester l'appartenance `a cette liste. 
     * @return vrai si <tt>p</tt> appartient `a cette liste de processus
     */
    /*@
      @ requires p != null;
      @
      @ ensures \result <==> plist.contains(p);
      @*/
    public /*@ pure @*/ boolean contientProcessus(Processus p);
}