ejercicio 15 Despues de las correcciónes del miercoles.

Che, estuve viendo el ejercicio 15 de vuela, y me parece que estaba faltando esto, diganme si me equivoco.


15.
problema AgregarTemaSA( t: Tema , s: SA) {
requiere (¥ t' <- temas(s) , ¬ ( ( nombres(t) == nombres (t') ) y mismos (etiquetas(t), etiquetas(t'))
modifica s
asegura (existe e <- (etiquetas (t) ) ¬ (en ( etiquetas (s)) --> etiquetas(s) == etiquetas(pre(s)) ++ [ e | e <-- etiquetas (t), ¬ (en ( etiquetas (s)) ];
asegura ¬(existe e <- (etiquetas (t) ) ¬ (en ( etiquetas (s)) --> etiquetas (s) == etiquetas(pre(s));
asegura mismos (temas (s) , temas (pre(s)) ++ t);

Los en estan mal.

dice en ( etiquetas (s)) deberia decir, en (e, etiquetas(s)), una boludez, y creo que lo que dijo nico esta bien

problema AgregarTemaSA( t: Tema , s: SA) {
requiere (¥ t' <- temas(s) , ¬ ( ( nombres(t) == nombres (t') ) y mismos (etiquetas(t), etiquetas(t'))
modifica s
asegura (existe e <- (etiquetas (t) ) ¬ (en ( e,etiquetas (s)) --> etiquetas(s) == (etiquetas(pre(s)) ++ [ e | e <-- etiquetas (t), ¬ (en ( e, etiquetas (s))) ];
asegura ¬(existe e <- (etiquetas (t) ) ¬ (en (e, etiquetas (s)) --> etiquetas (s) == etiquetas(pre(s));
asegura mismos (temas (s) , temas (pre(s)) ++ t);

FALTA PONER QUE SI EL TEMA TIENE LOS MISMOS DATOS QUE OTRO EN EL SA NO LO AGREGUE(OSEA QUE LA OPERACION NO TIENE EFECTO)

problema AgregarTemaSA( t: Tema , s: SA) {
requiere (¥ t' <- temas(s) , ¬ ( ( nombres(t) == nombres (t') ) y mismos (etiquetas(t), etiquetas(t'))
modifica s
asegura If (¥ t' <- temas(s)) ¬TemasIguales (t,t') Then (existe e <- (etiquetas (t) ) ¬ (en ( e,etiquetas (s)) --> etiquetas(s) == (etiquetas(pre(s)) ++ [ e | e <-- etiquetas (t), ¬ (en ( e, etiquetas (s))) ] Else etiquetas (s) == pre (s);
asegura ¬(existe e <- (etiquetas (t) ) ¬ (en (e, etiquetas (s)) --> etiquetas (s) == etiquetas(pre(s)); // en este no me cambia nada que agregue el tema o no.;
asegura If (¥ t' <- temas(s)) ¬TemasIguales (t,t') Then mismos (temas (s) , temas (pre(s)) ++ t) Else mismos (temas (s), temas (pre(s));

quedo mezclado IF Then ELse con implicas... alguien se opone?