uv16472

Montrez par les tableaux sémantiques que la formule 'A' x : (p(x) -> 'A' z : (p(z) -> 'E' y : gt(x,y,z))) est conséquence logique de la formule 'A' x : (p(x) -> 'E' y : 'A' z : (p(z) -> gt(x,y,z)))

lmM(a , 'A').
lmM(b , 'B').
lmM(c , 'C').
lmM(d , 'D').
lmM(e , 'E').
lmM(f , 'F').
lmM(g , 'G').
lmM(h , 'H').
lmM(i , 'I').
lmM(j , 'J').
lmM(k , 'K').
lmM(l , 'L').
lmM(m , 'M').
lmM(n , 'N').
lmM(o , 'O').
lmM(p , 'P').
lmM(q , 'Q').
lmM(r , 'R').
lmM(s , 'S').
lmM(t , 'T').
lmM(u , 'U').
lmM(v , 'V').
lmM(w , 'W').
lmM(x , 'X').
lmM(y , 'Y').
lmM(z , 'Z').

Construire le programme Prolog mM/2 tel que

si X est une liste NON-vide de caractères et Y une variable alors  ?-  mM(X , Y). retourne Y la liste X en caractères majuscules.

si Y est une liste NON-vide de caractères et X une variable alors  ?-  mM(X , Y). retourne X la liste Yen caractères minuscules.

si X et Y sont des listes NON-vide de caractères  alors  ?-  mM(X , Y). réussit si X et Y sont des listes identiques à la casse près des caractères et échoue sinon.

Donc reprenons  ici cet exercice :

Enoncé : pour inverser un tableau d'entiers tab de n éléments indicés à partir de 0 on le copie "à l'envers" dans un  tableau de même dimension inv et on a obtenu le programme :

     //tab.length étant le nombre d'éléments du tableau tab
     {tab.length>0 &  'A' x :((x>=0 & x < tab.length ) -> typeof(tab(x))== int} 
     i := 0; 
     n := tab.length;  
     while( i !=n  )
     do{
        inv[i]= tab[n-i-1];
        i := i+1;
     }
  

QUESTION 1 : Donnez la post-condition de la boucle qui caractérise le résultat attendu.

QUESTION 2 : Donnez un invariant et un variant pour cette boucle.

QUESTION 3 : Montrez la correction totale de cette boucle selon le canevas habituel.

4-Java (7 points) :

On vous demande d'implémenter certaines des procédures de la classe Vecteur du package java.util en tenant compte des spécifications formelles et informelles fournies avant ces procédures. Dans le cas où les paramètres ne seraient pas conformes aux spécifications on lèvera des exceptions sous-classes de RuntimeException.

package java.util;
public class Vector extends AbstractList implements List, Cloneable, java.io.Serializable {

    protected /*@non_null*/ Object elementData[];

    /*@spec_public*/   protected int elementCount;

    //@ invariant 0 <= elementCount  &&  elementCount <= elementData.length ;

    // définit la valeur dont sera augmentée la taille de elementData 
   //en cas d'ajout trop important de données au vecteur
    protected int capacityIncrement;

    //@ requires initialCapacity >= 0 &&  capacityIncrement >= 0 ;
    //@ ensures this.elementCount == 0
    //@ ensures this. elementData.length == initialCapacity
    //@ ensures this.capacityIncrement == capacityIncrement
    public Vector(int initialCapacity, int capacityIncrement) {…}

   //Crée un vecteur constitué des éléments de la collection passée en paramètre
   // this.capacityIncrement sera de 10% de la taille de la collection
    public Vector(/*@non_null*/ Collection c) {…}

    //@ requires 0 <= index && index < elementCount ;
    //@ ensures \result==this.elementData[index]
    public Object elementAt(int index) {…}  

   


    //@ modifies elementCount,elementData,elementData[elementCount]
    //@ ensures  elementCount == \old(elementCount)+1
    public void addElement(Object obj) {…}

                    // retourne un objet énumération des éléments du vecteur
    public Enumeration elements;

  //@ invariant (\forall Vector v; v==null || v==this  || v.elementData!=this.elementData) 
}

Question 1 : Implémenter le constructeur d'arité 2  public Vector(int initialCapacity, int capacityIncrement) {…}

                              // suggestion : System.arraycopy(oldData, 0, elementData, 0, elementCount);

Rappel : public Enumeration elements() {

return new Enumeration() {

… };

}