gestionProc
Interface ProcessusList

All Known Implementing Classes:

ProcessusFIFO, ProcessusPrio

public interface ProcessusList

Repr'esentation d'une liste contenant des processus non nuls.
Une telle liste ne contient pas deux processus de meme identifiant.
Il est possible :

• de d'eterminer si un processus d'identifiant donn'e appartient `a cette liste;
• d'ajouter un processus `a la liste (sans pr'eciser o`u se fait l'insertion);
• de retirer un processus de la liste (sans pr'eciser lequel).

Class Specifications

public invariant this.plist != null;

Specifications inherited from class Object

public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  java.util.List	plist

 

Method Summary
void	ajouterProcessus(Processus p)           Ajoute le processus p dans cette liste de processus.
boolean	contientProcessus(Processus p)           Retourne vrai si cette liste contient le processus p.
boolean	empty()           Retourne vrai si cette liste de processus est vide.
int	nbElem()           Retourne le nombre d''el'ements de cette liste de processus.
Processus	retirerProcessus()           Retire un processus de cette liste et le retourne.

 

Model Field Detail

plist

public java.util.List plist

Specifications: instance
datagroup contains: gestionProc.ProcessusFIFO.maListe gestionProc.ProcessusPrio.maListe

empty

public boolean empty()

Retourne vrai si cette liste de processus est vide.

Returns:

vrai si le nombre d''el'ements de cette liste vaut 0

Specifications: pure

ensures \result <==> this.plist.isEmpty();

nbElem

public int nbElem()

Retourne le nombre d''el'ements de cette liste de processus.

Returns:

le nombre d''el'ements de cette liste

Specifications: pure

ensures \result == this.plist.size();

ajouterProcessus

public void ajouterProcessus(Processus p)

Ajoute le processus p dans cette liste de processus. M'ethode non-d'eterministe : l'emplacement de l'insertion n'est pas pr'ecis'e.

Parameters:

p - un processus `a ajouter `a la liste

Specifications:

requires p != null;
requires !this.plist.contains(p);
assignable plist;
ensures \old(this.plist.size()) == this.plist.size()-1;
ensures ( \forall int i; i >= 0&&i < \old(this.plist.size()); this.plist.contains(\old(this.plist.get(i))));
ensures this.plist.contains(p);

retirerProcessus

public Processus retirerProcessus()

Retire un processus de cette liste et le retourne. M'ethode non-d'eterministe : ne pr'ecise pas quel processus est retir'e.

Returns:

un processus de la liste

Specifications:

requires !this.empty();
assignable plist;
ensures \old(this.plist.size()) == this.plist.size()+1;
ensures ( \forall int i; i >= 0&&i < \old(this.plist.size()); \old(this.plist.get(i)).equals(\result )||this.plist.contains(\old(this.plist.get(i))));
ensures !this.plist.contains(\result );

contientProcessus

public boolean contientProcessus(Processus p)

Retourne vrai si cette liste contient le processus p.

Parameters:

p - le processus dont on souhaite tester l'appartenance `a cette liste.

Returns:

vrai si p appartient `a cette liste de processus

Specifications: pure

requires p != null;
ensures \result <==> this.plist.contains(p);