Práctica 4, Ej 15

I)
problema nEsimaAparicion(l : [T],e : T,n: Int) = res : Int {
requiere |l|>0 ;
requiere n<=|l| ;
requiere en(l,e) ;
requiere 0<n<cuenta(l,e) ;
asegura res==cuenta(e,listaHastaElIndice) ;
aux listaHastaElIndice : [T] = [indice(l,i) | i <-- [0..res]] ;
}

II)
problema subCadena(s,t : [T]) = res : Bool {
requiere |s|>0 ;
requiere |t|>0 ;
asegura res == alguno( [contenidaEntre(i,j) | i,j <-- [0..|t|)) ;
aux contenidaEntre(i,j : Int) : Bool = s==[indice(t,k) | k <-- [i..j]] ;
{

III)
problema incluida(s,t : [T]) = res : Bool {
asegura res== Existencia && Cantidad ;
aux Existencica : Bool = todos([en(x,t) | x <-- s]) ;
aux Cantidad : Bool = todos([cuenta(s,i)<=cuenta(t,i) | i <-- s]) ;
}

IV)
problema mezclarOrdenado(s,t : [Int]) = res : [Int] {
asegura |res|==|s|+|t| ;
asegura s==[res(i) | i <-- [0..|res|), i mod 2 == 0] ;
asegura t==[res(j) | j <-- [0..|res|), i mod 2 == 1] ;
}

V)
problema intersección(s,t : [T]) = res: [T] {
asegura todos( [cuenta(res,x)=max(cuenta(res,s),cuenta(res,t)) | x <-- t ] ) ;
segura todos( [en(x,res) | x <-- s, en(x,t)] ) ;
asegura todos( [en(x,res) | x <-- t, en(x,s)] ) ;
aux max(n,m : Int) : Int = beta(n>=m)*n + beta(n<m)*m ;
{

VI)
problema intersecciónOrdenada(s,t : [T]) = res: [T] {
asegura todos( [cuenta(res,x)=max(cuenta(res,s),cuenta(res,t)) | x <-- t ] ) ;
segura todos( [en(x,res) | x <-- s, en(x,t)] ) ;
asegura todos( [en(x,res) | x <-- t, en(x,s)] ) ;
asegura todos( [indicePrimeraAparicion(x,s)<indicePrimeraAparicion(y,s) | x,y <-- s , indicePrimeraAparicion(x,res)<indicePrimeraAparicion(y,res)] )
aux indicePrimeraAparicion(e : T, l : [T]) : Int ) cabeza([i| i <-- [0..|s|) , indice(s,i)==e])
aux max(n,m : Int) : Int = beta(n>=m)*n + beta(n<m)*m ;
{

Hola, yo encontre algunos errores en los tuyos, por lo que los resolví un poco diferente, compara con los mios y cualquier cosa discutimos los resultados...

1-
Problema nEsimaAparicion\((l:[T],e:T,n:Z)=res:Z\){
requiere: \(0<n\leq{cuenta(l,e)};\)
requiere: \(e\in{l};\)
asegura: \(a_{res}==e;\)
asegura: \(\forall{i\leftarrow{[0...|res|)}}, cuenta(l,e)==n-1;\)
}

3-
Problema incluida\((s,t:[T])=res:Bool\){
requiere: \(|s|\leq{|t|};\)
asegura: \(res==(\forall{x\leftarrow{s}})(\exists{y\leftarrow{t}}), x==y\;,cuenta(s,x)\leq{cuenta(t,x)};\)
}

4-
Problema mezclarOrdenado\((s,t:[Z])=res:[Z]\){
requiere: |s|==|t| && |s|>0;
asegura: |res|==|s|+|t|;
asegura: \(s==[res_i | i\leftarrow{[0...|res|)}, i\;mod\;2==0];\)
asegura: \(t==[res_j | j\leftarrow{[0...|res|)}, j\;mod\;2==1];\)
}

5-
Problema interseccion\((s,t:[T])=res:[T]\){
asegura: \((\forall{x\leftarrow{res}}), x\in{s}\;y\;x\in{t};\)
asegura: \(cuenta(res,x)==menor(cuenta(s,x),cuenta(t,x));\)
aux menor\((a,b:Z):Z=if a\leq{b}\;then\;a\;else\;b;\)
}

6-
Problema interseccionOrdenada\((s,t:[T])=res:[T]\){
asegura: \((\forall{x\leftarrow{res}}), x\in{s}\;y\;x\in{t};\)
asegura: \(cuenta(res,x)==menor(cuenta(s,x),cuenta(t,x));\)
asegura: \((\forall{i\leftarrow{[0...|res|)}})(\exists{j\leftarrow{[0...|s|)},r\leftarrow{[0...|t|)}}),res_i==s_j==t_r\)&&\(j\leq{r};\)
aux menor\((a,b:Z):Z=if a\leq{b}\;then\;a\;else\;b;\)
}

Perdón que no contestaba, no tenía "monitoreado" el topic.

Creo que los tuyos funcionan, los míos los tendría que ver porque los hice hace un tiempito. En una hora y media es el parcial de especificación así que ya no creo que te interese mucho discutirlos. La semana que viene si querés discutimos Haskell 😈

Saludos y de nuevo perdón por no contestar!

en el 2do asegura del ultimo ejercicio no dijiste quien es x....(carla)

y me parece q eso d los indices no anda =S

proba con s=[1,6,0,3] t=[0,5,6,1] deberia dar [1,6,0]

cuando todos los indices toman la posicion 0...no valen lo mismo