A ver que les parece mi idea.
Como la función debe devolver una posición válida en caso de cumplirse la condición exigida, es necesario que el vector de entrada tenga al menos 1 elemento.
Por tanto, la precondición sobre los datos de entrada podría ser {Q= n>0}
La signatura o perfil podría ser:
fun posneg ( v: vect [1..n] de ent) dev pos: nat;
En la postcondición debemos exigir a nuestra función que devuelva la primera posición del valor menor que cero.
R= Existe un alfa perteneciente desde [1..n] tal que si v[alfa]<0 ----> pos=alfa)
Este predicado podría darnos problemas si existe más de un valor que cumpla la condición requerida por lo que, a mi entender, se hace necesario un segundo conjuntante utilizando el cuantificador universal que nos garantice que [B]pos [/B]es la primera posición que cumple la condición:
AND Para todo alfa perteneciente desde {v[pos]+1.. n] tal que [B]pos[/B] no es igual a alfa.
En iterativo el código podría ser algo parecido a:
i:=1 (Inicialización de la variable de protección del bucle)
pos:=0;
Mientras i<=n hacer
Si v[i]< 0 ---> pos:=i; EXIT;
Si no i++;
Fmientras;
dev pos;
En recursiva la función podría ser algo parecido a :
fun iposneg ( v: vect [1..n] de ent , i:nat) dev pos:nat;
Caso trivial i=0 ----> pos:=0;
Caso no trivial i>0 ---> iposneg( v, i-1) OR (v[i]<0 ---> pos=i);
Fcaso;
Ffun;
Salúos.
__________________
Última edición por al-mo; 10/06/2010 a las 00:12.
|