1- Preuves : Soit montrer : [ 'A' x : (p(x) -> 'E' y : 'A' z : (p(z) -> gt(x,y,z)))] |- 'A' x : (p(x) -> 'A' z : (p(z) -> 'E' y : gt(x,y,z)))

2- Prolog :

/* à gauche en minuscules , à droite en Majuscule */
mM([] , []).
mM([Xm|Lm] , [XM|LM]) :- lmM(Xm , XM) , !, mM(Lm , LM).
mM([X|Lm] , [X|LM]) :- mM(Lm , LM).

3-logique de Hoare :

   
       {  n>0}       

         i := 0 ;  

      {i==0  &  n>0}
       while ~(i =n)
              invariant {'A' x : ((x>=0 & x < i ) -> inv(x) =tab(n-x-1)) & i<=n}
              variant {n - i}
       do
       (
       inv[i]= tab[n-i-1];

       i := i+1;

       )
       end ;
     {'A' x : ((x>=0 & x < n) -> inv(x) =tab(n-x-1)) }

I :  {'A' x : ((x>=0 & x < i ) -> inv(x) =tab(n-x-1)) & i<=n}  & B : i != n

trivial : i+1<=n  ->   i<=n

{'A' x : ((x>=0 & x < i ) -> inv(x) ==tab(n-x-1)) & i+1<=n  }

{'A' x : ((x>=0 & x < i ) -> inv(x) ==tab(n-x-1)) & i+1<=n   &  tab[n-i-1]==tab(n-i-1)}

    inv[i]= tab[n-i-1];

{'A' x : ((x>=0 & x < i ) -> inv(x) ==tab(n-x-1)) & i+1<=n   &   inv(i) ==tab(n-i-1)}

{'A' x : ((x>=0 & x < i +1) -> inv(x) ==tab(n-x-1)) & i+1<=n}

     i := i+1;

I : {'A' x : ((x>=0 & x < i ) -> inv(x) =tab(n-x-1)) & i<=n}

I : ('A' x : ((x>=0 & x < i ) -> inv(x) =tab(n-x-1)) & i<=n)  &  ~B : i==n  ->    'A' x : ((x>=0 & x < n) -> inv(x) =tab(n-x-1)) triviale

La correction partielle est vérifiée

{n-i-1<n-i} : toujours vérifiée

   V1:= n-i;

{n-i-1<V1}

     i := i+1;

{n-i<V1}

package java.util;

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

    //@ invariant \typeof(elementData) == \type(Object[])

    /*@ invariant (\forall int i; (0<=i && i<elementCount) ==> (\typeof(elementData[i]) <: elementType || elementData[i]==null)) */
    /*@ invariant (\forall int i; (0<=i && i<elementCount) ==> (!containsNull ==> elementData[i]!=null)) */

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

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

    //@ invariant 0 <= elementCount && elementCount <= elementData.length ;
    /*@spec_public*/ protected int elementCount;
   protected int capacityIncrement;
   private static final long serialVersionUID = -2767605614048989439L;
     */
    //@ requires initialCapacity >= 0 ;
    //@ ensures this.elementCount == 0
    public Vector(int initialCapacity, int capacityIncrement) {
	     super();
        if (initialCapacity < 0) throw new IllegalArgumentException("Illegal Capacity: " +  initialCapacity);
	     this.elementData = new Object[initialCapacity];
	     this.capacityIncrement = capacityIncrement;
	//@ set elementType = \type(Object)
	//@ set containsNull = true
    }

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

    //@ ensures this.elementCount == 0
    public Vector() {
	this(10);
    }

    //@ ensures this.elementType == c.elementType
    //@ ensures this.containsNull == c.containsNull
    public Vector(/*@non_null*/ Collection c) {
	      this((c.size()*110)/100);	// Allow 10% room for growth
	      //@ assume c.elementType <: \type(Object)
	      //@ set elementType = c.elementType
	      //@ set containsNull = c.containsNull
	      Iterator i = c.iterator();
	      while (i.hasNext()) elementData[elementCount++] = i.next();  //@ nowarn IndexTooBig
    }


...

    //@ ensures \result != null
    //@ ensures \result!=null
    //@ ensures \result.elementType == elementType
    //@ ensures \result.returnsNull == containsNull
    public Enumeration elements() {
	return new Enumeration() {
	    int count = 0;

	    public boolean hasMoreElements() {
		return count < elementCount;
	    }

	    public Object nextElement() {
		synchronized (Vector.this) {
		    if (count < elementCount) {
			return elementData[count++];
		    }
		}
		throw new NoSuchElementException("Vector Enumeration");
	    }
	};
    }

 ...
 
    //@ requires 0 <= index ;
    //@ requires index < elementCount ;
    //@ ensures \typeof(\result) <: elementType || \result==null
    //@ ensures !containsNull ==> \result!=null
    public synchronized Object elementAt(int index) {
	    if (index >= elementCount) {
	       throw new ArrayIndexOutOfBoundsException(index + " >= " + elementCount);
	   }

	   try {
	       return elementData[index];
	   } catch (ArrayIndexOutOfBoundsException e) {
	       throw new ArrayIndexOutOfBoundsException(index + " < 0");
	   }
    }

...

    //@ requires \typeof(obj) <: elementType
    //@ requires containsNull || obj!=null
    //@ modifies elementCount
    //@ ensures  elementCount == \old(elementCount)+1
    public synchronized void addElement(Object obj) {
	modCount++;
	ensureCapacityHelper(elementCount + 1);
	elementData[elementCount++] = obj;
    }
...

}