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)|) }