| Revisión actual |
Tu texto |
| Línea 356: |
Línea 356: |
| ''Usa'' Bool, Nat, Cinta | | ''Usa'' Bool, Nat, Cinta |
|
| |
|
| ''Exporta'' Genero, Generadores, Observadores básicos, Otras operaciones | | ''Exporta'' Genero, Generadores, Observadores, Otras operaciones |
|
| |
|
| ''Axiomas'' | | ''Axiomas'' |
| Línea 420: |
Línea 420: |
| ''Usa'' Bool, Nat | | ''Usa'' Bool, Nat |
|
| |
|
| ''Exporta'' Genero, Generadores, Observadores básicos, Otras operaciones | | ''Exporta'' Genero, Generadores, Observadores, Otras operaciones |
|
| |
|
| ''Otras operaciones'' | | ''Otras operaciones'' |
| Línea 491: |
Línea 491: |
|
| |
|
| == Ejercicio 12 == | | == Ejercicio 12 == |
|
| |
| TAD Producto es String
| |
|
| |
| '''TAD Stock'''
| |
|
| |
| ''Igualdad observacional''
| |
|
| |
| (∀ s1:stock)((∀ s2:stock)(s1 =obs s2 ⇔ ((∀ p:producto)(estaRegistrado(p,s1) ⇔ estaRegistrado(p,s2)) ∧L (∀ p1:producto)((∀ p2:producto)((estaRegistrado(p1,s1) ∧ estaRegistrado(p2,s1)) ⇒L (mínimo(p1,s1) = mínimo(p1,s2) ∧ compras(p1,s1) = compras(p1,s2) ∧ ventas(p1,s1) = ventas(p1,s2) ∧ esSus(p1,p2,s1) = esSus(p1,p2,s2)))))))
| |
|
| |
| ''Genero'' stock
| |
|
| |
| ''Usa'' Bool, Nat, Conj(α)
| |
|
| |
| ''Exporta'' Genero, Generadores, Observadores básicos, stocksBajos
| |
|
| |
| ''Observadores básicos''
| |
|
| |
| estaRegistrado: producto x stock → bool
| |
|
| |
| esSus: producto a x producto b x stock s → bool {estaRegistrado(a,s) ∧ estaRegistrado(b,s)}
| |
|
| |
| compras: producto p x stock s → nat {estaRegistrado(p,s)}
| |
|
| |
| ventas: producto p x stock s → nat {estaRegistrado(p,s)}
| |
|
| |
| mínimo: producto p x stock s → nat {estaRegistrado(p,s)}
| |
|
| |
| ''Generadores''
| |
|
| |
| crearStock: . → stock
| |
|
| |
| registrarProducto: producto p x nat x stock s → stock {¬ estaRegistrado(p,s)}
| |
|
| |
| comprar: nat x producto p x stock s → stock {estaRegistrado(p,s)}
| |
|
| |
| vender: nat n x producto p x stock s → stock {estaRegistrado(p,s) ∧L compras(p,s) ≥ n}
| |
|
| |
| infSus: producto a x producto b x stock s → stock {(estaRegistrado(a,s) ∧ estaRegistrado(b,s)) ∧L ¬(∃ p:producto)(esSus(p,b,s)) ∧ a ≠ b}
| |
|
| |
| ''OtrasOperaciones''
| |
|
| |
| stocksBajos: stock → conj(producto)
| |
|
| |
| tieneSus: producto p x stock s → bool {estaRegistrado(p,s)}
| |
|
| |
| obtenerSus: producto p x stock s → producto {estaRegistrado(p,s) ∧L tieneSus(p,s)}
| |
|
| |
| productos: stock → conj(producto)
| |
|
| |
| quitarBuenos: conj(producto) x stock → conj(producto)
| |
|
| |
| ''Axiomas''
| |
|
| |
| estaRegistrado(p,crearStock) ≡ false
| |
|
| |
| estaRegistrado(p,registrarProducto(a,n,s)) ≡ p = a ∨ estaRegistrado(p,s)
| |
|
| |
| estaRegistrado(p,comprar(n,a,s)) ≡ estaRegistrado(p,s)
| |
|
| |
| estaRegistrado(p,vender(n,a,s)) ≡ estaRegistrado(p,s)
| |
|
| |
| estaRegistrado(p,infSus(a,b,s)) ≡ estaRegistrado(p,s)
| |
|
| |
| compras(p,comprar(n,a,s)) ≡ if p = a then n + compras(p,s) else compras(p,s) fi
| |
|
| |
| compras(p,registrarProducto(a,n,s)) ≡ if p = a then 0 else compras(p,s) fi
| |
|
| |
| compras(p,vender(n,a,s)) ≡ compras(p,s)
| |
|
| |
| compras(p,infSus(a,b,s)) ≡ compras(p,s)
| |
|
| |
| ventas(p,vender(n,a,s)) ≡ if p = a then n + ventas(p,s) else ventas(p,s) fi
| |
|
| |
| ventas(p,registrarProducto(a,n,s)) ≡ if p = a then 0 else ventas(p,s) fi
| |
|
| |
| ventas(p,comprar(n,a,s)) ≡ ventas(p,s)
| |
|
| |
| ventas(p,infSus(n,a,s)) ≡ ventas(p,s)
| |
|
| |
| esSus(a,b,registrarProducto(c,n,s)) ≡ if a = c ∨ b = c then false else esSus(a,b,s) fi
| |
|
| |
| esSus(a,b,infSus(c,d,s)) ≡ (a = c ∧ b = d) ∨ esSus(a,b,s)
| |
|
| |
| esSus(a,b,comprar(n,c,s)) ≡ esSus(a,b,s)
| |
|
| |
| esSus(a,b,vender(n,c,s)) ≡ esSus(a,b,s)
| |
|
| |
| mínimo(p,registrarProducto(a,n,s)) ≡ if p = a then n else mínimo(p,s) fi
| |
|
| |
| mínimo(p,comprar(n,a,s)) ≡ mínimo(p,s)
| |
|
| |
| mínimo(p,vender(n,a,s)) ≡ mínimo(p,s)
| |
|
| |
| mínimo(p,infSus(a,b,s)) ≡ mínimo(p,s)
| |
|
| |
| stocksBajos(s) ≡ quitarBuenos(productos(s),s)
| |
|
| |
| productos(crearStock) ≡ ∅
| |
|
| |
| productos(comprar(n,a,s)) ≡ productos(s)
| |
|
| |
| productos(vender(n,a,s)) ≡ productos(s)
| |
|
| |
| productos(registrarProducto(a,n,s)) ≡ Ag(a,productos(s))
| |
|
| |
| productos(infSus(a,b,s)) ≡ productos(s)
| |
|
| |
| tieneSus(p,registrarProducto(a,n,s)) ≡ (¬ p = a) ∧L tieneSus(p,s)
| |
|
| |
| tieneSus(p,comprar(n,a,s)) ≡ tieneSus(p,s)
| |
|
| |
| tieneSus(p,vender(n,a,s)) ≡ tieneSus(p,s)
| |
|
| |
| tieneSus(p,infSus(a,b,s)) ≡ p = b ∨ tieneSus(p,s)
| |
|
| |
| obtenerSus(p,infSus(a,b,s)) ≡ if p = b then a else obtenerSus(p,s) fi
| |
|
| |
| obtenerSus(p,registrarPruducto(a,n,s)) ≡ obtenerSus(p,s)
| |
|
| |
| obtenerSus(p,comprar(n,a,s)) ≡ obtenerSus(p,s)
| |
|
| |
| obtenerSus(p,vender(n,a,s)) ≡ obtenerSus(p,s)
| |
|
| |
| quitarBuenos(∅,s) ≡ ∅
| |
|
| |
| quitarBuenos(Ag(p,c),s) ≡ if tieneSus(p,s) then if mínimo(p,s) > compras(p,s) + compras(obtenerSus(p,s),s) - ventas(p,s) - ventas(obtenerSus(p,s),s) then Ag(p,quitarBuenos(c,s)) else quitarBuenos(c,s) fi else if mínimo(p,s) > compras(p,s) - ventas(p,s) then Ag(p,quitarBuenos(c,s)) else quitarBuenos(c,s) fi
| |
|
| |
| '''Fin TAD'''
| |
|
| |
|
| == Ejercicio 13 == | | == Ejercicio 13 == |
