Lo que tenemos hasta ahora (10/09) (Revisados 1 vez)

PARTE 3 (Tema)


0. Invariante NoHayEtiquetasRepetidas


1
problema crearTema(n:Nombre, l: [Etiqueta], d: Datos) = result : Tema {
asegura nombre (result) == n;
asegura mismos(l, etiquetas(result));
asegura datos (result) == d;
}

2
problema nombreT(t:Tema) = result :Nombre{
asegura result == nombre(t);
}

3
problema etiquetasT(t:Tema) = result:[Etiquetas] {
asegura result == etiquetas(t);
}

4.
problema datosT(t :Tema) = result : Datos{
asegura result = = Datos (t);
}

5.
problema igual (t, t’: Tema) = result : Bool {
asegura result == TemasIguales (t, t');
}

6.

problema menorT (l:[Etiquetas], t, t':Tema) = result : Bool {
asegura result == (toBin(l, t) <bin toBin(l, t')) o ((toBin(l, t) =bin toBin(l, t')) y (nombtre(t) <= nombre(t')));
}

(opcional) problema menorT (l:[Etiquetas], t, t':Tema) = result : Bool {
asegura result == If toBin(t) =bin toBin(t’) Then nombre (t) < = nombre (t’) Else toBin(t); <bin toBin(t’);
}



PARTE 4 (SA)


7.
invariante noHayEtiquetasRepetidas: (¥ i←[0...|etiquetas(s)|)) (¥j←[0...|etiquetas(s)|),i!=j) etiqueta(s)[i]!=etiqueta(s)[j];

8.
invariante lasEtiquetasDeLosTemasSonEtiquetasValidas: (¥ t←temas(s)) Incluido(etiquetas (t), etiquetas (s));

9.
invariante noHayTemasConLosMismosDatos: ( ¥ i <- [0..|temas(s)|)) ( ¥ j <- [ 0..|temas(s)|, i != j) ¬ (TemasIguales( temas(s)[i], temas(s)[j] );
10.
invariante noHayTemasConLosMismosNombresYEtiquetas: (¥ t←[temas(s)])(¥ t'←[temas(s)], ¬Temasiguales(t,t')) ((toBin( etiquetas (s),t)!=bin toBin( etiquetas(s), t’)) o (nombre(t) != nombre(t')));

DECISION : TOMAMOS EL IGUAL CON TUBIN EN VEZ DE "MISMOS" PORQUE QUISIMOS QUE NO SE TENGAN EN CUENTA LAS ETIQUETAS REPETIDAS EN LOS TEMAS.

11.
problema crear SA () =result :SA {

asegura etiquetas (result) == [];
asegura temas (result) == [] ;
}



12.
problema etiqueta (s:SA) = result : [etiqueta]{
asegura mismos(etiquetas(s),result);
}

13.
problema temasSA(l:[Etiqueta],s:SA) = result :[Nombre]{
asegura result == [ nombre (h) | h <- OrdenaT(temas(s)) , incluido ( EtiquetasValidadas(l), etiquetas (h)]
}

14.
problema ordenSA (t:Tema, s:SA) = result : Int {
Requiere en (t, temas(s));
Asegura result == | [t | t’ ← temas(s), menorT (etiquetas(s), t’,t) y ¬TemasIguales (t,t’)] | ;
}

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 mismos (temas (s) , temas (pre(s)) ++ t)


AUXILIARES:


aux pertenece(t:T,a:[T]) Bool=
(E t’←a))t’= =t;//Lo volví a definir, no lo encontré en los que anoté yo, no se pierde nada con rehacerlo.

aux CuantasListas(t:Tema) Int =
|etiquetas(t)|;

aux Mayor(a: Z ,b:[Z]): Bool =
(¥ x←b)a>=x;

aux TemasIguales ( t, t' : Tema) : Bool =
(datos (t) ==datos (t'))

aux Incluido (a,b :[T]): Bool ==
( ¥ i <-[0...|a|) ) ( existe j <- [0...|b|) ) a[i]==b[j]

aux OrdenEnListaDeRep (t:Tema, r:Reproductor) =
| [t’ | t’ ← temas(archivos(s), mismos (etiquetas(t), sgd(estado(r)) , menorT (etiquetas(s), t’,t) ¬TemasIguales (t,t’)] | + 1;

aux PrimerTemaDeLaListaDeRep (l:ListaDeReproduccion, r:Reproductor):Tema =
cab [ x | x ← temas(archivos(r)), OrdenEnListaDeRep == 1]

aux Union (t,t’:: [T]):[T] =
t ++ [x | x ← t’, ¬en(x,t)];


aux OrdenEtiqueta (e: Etiqueta, s: SA):Int =
cab[i | i ← [0.. |etiquetas(s)|), eitquetas(s)[i] == e];

aux ToBin (l:[etiqueta], t:Tema) :[Int] =
[β( ( Existe e <- etiquetas(t) )e == l[i])| i <-[0...|l|) ]

aux <bin(b1,b2:[Int]):Bool =
if ( (¥ h <- b1 ) h == 1 o h == 0) y ( (¥ h <- b2 ) h == 1 o h == 0 )
then (ToDecimal (b1) < ToDecimal (b2))

aux =bin(b1,b2:[Int]):Bool =
if ( (¥ h <- b1 ) h == 1 o h == 0) y ( (¥ h <- b2 ) h == 1 o h == 0 )
then (ToDecimal (b1) == ToDecimal (b2))

aux ToDecimal (b:[Int]) :Int =
if (¥ h <- b ) h == 1 o h == 0
then ∑[ b[i]*(pot(2,i))| i <- [0...|b|)]

aux OrdenaT(l :[Etiquetas] , t: [Temas]) : [Temas] =
acum ( conc (r,[h]) | r: [Temas]=[] , h <- t , h == maxBin (l , Resta ( temas(s) , r) )

aux maxBin ( e : [etiquetas] , t : [Temas] ): Tema =
cab [ x | x <- temas(s) , ( ¥ x' <- temas(s), ¬ (TemasIguales ( x, x')) ) ToBin (x') <bin ToBin (x) ]

aux Resta (a,b [T]) : [T] =
[ h | h <- a , ¬ (en ( h , b) ) ]

aux ValidarEtiquetas( e: [etiquetas] , s :SA ) : [etiquetas] =
[ x | x <- e , en (x, etiquetas (s))]

aux MenorT (l : [etiquetas] , t, t': Tema ) : Bool =
(toBin(l, t) <bin toBin(l, t')) o ((toBin(l, t) =bin toBin(l, t')) y (nombtre(t) <= nombre(t')));