void Lista::eliminarPosicion(int pos){ int i = 0, j = pos + 1; lista listaAux; //Estado inicialC1 //vale this == pre(this) && listaAux == [] && i == 0 && 0 <= pos <= |this| while(i < pos){ //invariante: 0 <= i <= pos && this == pre(this) && listaAux == this[0..i) // variante pos - i; listaAux.agregarAtras(this.iesimo(i)); i++; } //QC1: listaAux == pre(this)[o..pos) //estado LuegoC1 //vale this == pre(this) // vale QC1 //Estado inicialC2 //vale j == pos + 1 && listaAux == pre(this)[0..pos) && this == pre(this) while(j < this.longitud()){ //invariante: pos + 1 <= j <= |pre(this)| //variante |pre(this)| - j listaAux.agregarAtras(this.iesimo(j)); j++; } //QC2: listaAux == pre(this)[0..pos) ++ pre(this)(pos.. |pre(this)|) this = listaAux; //vale this == pre(this)[0..pos) ++ pre(this)(pos.. |pre(this)|) } int posicion(const T & e) const { int i = 0; //Estado AntesC; // vale i == 0 && e (pertenece) this && |this| >= 0 while( i < this.length() && this.iesimo(i) != e) { //invariante I: 0 <= i <= |this| && ((paratodo) x <- [0.. i)) this [x] != e // variante v:|this| - i //Estado 1 ++i; //Estado 2 } return i; //Estado DespuesC //vale Q: cab([i| x <- [0.. |this|), this[x] == e])