guia04.txt

/* apunte oficial TADs 2c 2023: https://campus.exactas.uba.ar/pluginfile.php/509550/mod_resource/content/1/tads.pdf */

TAD Conjunto<T> {
    obs elems: conj<T>

    proc conjVacio(out c: Conjunto<T>) {
        requiere {True}
        asegura {c.elems == {}}
    }

    proc agregar(inout c: Conjunto<T>, in e: T) {
        requiere {c == old(c)}
        asegura {c.elems == old(c).elems + {e}}
    }

    proc quitar(inout c: Conjunto<T>, in e: T) {
        requiere {c == old(c)}
        asegura {c.elems == old(c).elems - {e}}
    }
}

TAD Punto {
    obs x: real
    obs y: real

    proc nuevoPunto(in px: real, in py: real, out p: Punto) {
        requiere {True}
        asegura {p.x == px && p.y == py}
    }

    proc coordX(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.x}
    }

    proc coordY(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.y}
    }

    proc coordTheta(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == safearctan(p.x, p.y)}
    }

    proc coordRho(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == sqrt(p.x**2 + p.y**2)}
    }

    proc mover(inout p: Punto, in deltaX, deltaY: real) {
        requiere {p == old(p)}
        asegura {p.x == old(p) + deltaX && p.y == old(p) + deltaY}
    }

    aux safearctan(x, y: real): real = if x == 0 then signo(y)*pi/2 else arctan(y/x) fi
}

1.a.
TAD Rectangulo2D {
    obs cs: tupla<struct<x: R, y: R>, struct<x: R, y: R>, struct<x: R, y: R>, struct<x: R, y: R>>

    proc crear(in c1x, c1y, c2x, c2y, c3x, c3y, c4x, c4y: real, out r: Rectangulo2D) {
        requiere {True}
        asegura {r.cs == <<x: c1x, y: c1y>, <x: c2x, y: c2y>, <x: c3x, y: c3y>, <x: c4x, y: c4y>>}  
    }

    proc trasladar(inout r: Rectangulo2D, in dx: real, in dy: real) {
        requiere {r == old(r)}
        asegura {forall i: int :: (0 <= i < 4) ==>L (r.cs[i].x == old(r).cs[i].x + dx && r.cs[i].y == old(r).cs[i].y + dy)}
    }

    proc escalar(inout r: Rectangulo2D, in k: real) {
        requiere {r == old(r) && k > 0}
        asegura {forall i: int :: (0 <= i < 4) ==>L (r.cs[i].x == k*old(r).cs[i].x && r.cs[i].y == k*old(r).cs[i].y)}
    }

    proc rotar(inout r: Rectangulo2D, in a: real) {
        requiere {r == old(r)}
        asegura {
            forall i: int :: (0 <= i < 4) ==>L 
                (r.cs[i].x == cos(a)*old(r).cs[i].x - sin(a)*old(r).cs[i].y && r.cs[i].y == sin(a)*old(r).cs[i].x + cos(a)*old(r).cs[i].y)
        }
    }

    proc invertir(inout r: Rectangulo2D) {
        requiere {r == old(r)}
        asegura {forall i: int :: (0 <= i < 4) ==>L (r.cs[i].x == -old(r).cs[i].x && r.cs[i].y == -old(r).cs[i].y)}
    }
}

1.b.
TAD Esfera3D {
    obs pos: struct<x: R, y: R, z: R>
    obs r: R

    proc crear(in x_, y_, z_, r_: real, out e: Esfera3D) {
        requiere {True}
        asegura {e.pos == <x: x_, y: y_, z: z_> && e.r == r_}
    } 

    proc trasladar(inout e: Esfera3D, in dx: real, in dy: real, in dz: real) {
        requiere {e == old(e)}
        asegura {e.pos.x == old(e).pos.x + dx && e.pos.y == old(e).pos.y + dy && e.pos.z == old(e).pos.z + dz}
        asegura {e.r == old(e).r}
    }

    proc rotar(inout e: Esfera3D, a1: real, a2: real) {
        /* a1 rota sobre el plano XY (alrededor del eje Z), a1 sobre el plano YZ (alrededor del eje X)*/
        requiere {e == old(e)}
        asegura {
            e.pos.x == cos(a1)*old(e).pos.x - sin(a1)*old(e).pos.y && 
            e.pos.y == cos(a2)*rotacion_XY_y(old(e).pos.x, old(e).pos.x, a1) - sin(a2)*old(e).pos.z
            e.pos.z == sin(a2)*rotacion_XY_y(old(e).pos.x, old(e).pos.x, a1) + cos(a2)*old(e).pos.z
        }
        asegura {e.r == old(e).r}
    }

    proc escalar(inout e: Esfera3D, k: real) {
        requiere {e == old(e) && k > 0}
        asegura {e.r == k*old(e).r}
        asegura {e.pos == old(e).pos}    
    }

    proc invertir(inout e: Esfera3D) {
        requiere {e == old(e)}
        asegura {e.pos.x == -old(e).pos.x && e.pos.y == -old(e).pos.y && e.pos.z == -old(e).pos.z}
        asegura {e.r == old(e).r}
    }

    aux rotacion_XY_y(in x, y, a: real): real = sin(a)*x + cos(a)*y
}

2.a.
/* el enunciado no aclara qué procedimientos especificar, así que voy a basarme en el TAD Conjunto visto en clase */
TAD Multiconjunto<T> {
    obs cantidad(e: T): int
    
    proc crear(out mc: Multiconjunto<T>) {
        requiere {True}
        asegura {forall e: T :: mc.cantidad(e) = 0}
    }

    proc agregar(inout mc: Multiconjunto<T>, in e: T) {
        requiere {mc == old(mc)}
        asegura {mc.cantidad(e) == old(mc).cantidad(e) + 1}
        asegura {forall elem: T :: elem != e ==> mc.cantidad(elem) = old(mc).cantidad(elem)}
    }

    proc remover_uno(inout mc: Multiconjunto<T>, in e: T) {
        requiere {mc == old(mc)}
        asegura {old(mc).cantidad(e) > 0 ==> mc.cantidad(e) == old(mc).cantidad(e) - 1}
        asegura {old(mc).cantidad(e) <= 0 ==> mc.cantidad(e) == 0}
        asegura {forall elem: T :: elem != e ==> mc.cantidad(elem) == old(mc).cantidad(elem)}
    }

    proc remover_todos(inout mc: Multiconjunto<T>, in e: T) {
        requiere {mc == old(mc)}
        asegura {mc.cantidad(e) = 0}
        asegura {forall elem: T :: elem != e ==> mc.cantidad(elem) == old(mc).cantidad(elem)}
    }

    proc pertenece(in mc: Multiconjunto<T>, in e: T, out res: bool) {
        requiere {True}
        asegura {res == True <==> mc.cantidad(e) > 0}
    }

    proc cantidad_elementos_totales(in mc: Multiconjunto<T>, out res: int) {
        sum e: T :: True :: mc.cantidad(e)
    }
}

2.b.
TAD Multidict<K, V> {
    obs pares: dict<K, conj<V>>

    proc crear(out md: Multidict<K, V>) {
        requiere {True}
        asegura {md.pares == {}}
    }

    proc acceder(in md: Multidict<K, V>, in k: K, out res: conj<V>) {
        requiere {k in md.pares}
        asegura {res == md.pares[k]}
    }

    proc crear_resetear_par(inout md: Multidict<K, V>, in k: K, in v: V) {
        requiere {md == old(md)}
        asegura {md.pares == setKey(old(md).pares, k, {v})}
    }

    proc remover_par(inout md: Multidict<K, V>, in k: K) {
        requiere {md == old(md)}
        asegura {md.pares == delKey(old(md).pares, k)} /* obs. asumo que delKey no hace nada si !(k in md) */
    }

    proc agregar_valor(inout md: Multidict<K, V>, in k: K, in v: V) {
        requiere {md == old(md)}
        asegura {md.pares == setKey(old(md).pares, k, old(md).pares[k].elems + {v})}
    }

    proc remover_valor(inout md: Multidict<K, V>, in k: K, in v: V) {
        requiere {md == old(md) && k in md.pares}
        asegura {md.pares == setKey(old(md).pares, k, old(md).pares[k].elems - {v})}
    }
}

3.a.
TAD CacheTTL<K, V> {
    obs datos: dict<K, V>
    obs tiempos_agregado: dict<K, real>
    obs ttl: real

    proc crear(in ttl_: real, out c: CacheTTL<K, V>) {
        requiere {ttl_ > 0}
        asegura {c.datos == {} && c.ttl == ttl_ && c.tiempos_agregado == {}}
    }
    
    proc esta(in c: CacheTTL<K, V>, in k: K) {
        requiere {True}
        asegura {res == True <==> (k in c.datos &&L now() - c.tiempos_agregado[k] < c.ttl)}
    }
    
    proc definir(inout c: CacheTTL<K, V>, in k: K, in v: V) {
        requiere {c == old(c)}
        asegura {c.datos == setKey(old(c).datos, k, v) && c.tiempos_agregado == setKey(old(c).tiempos_agregado, k, now()) && c.ttl == old(c).ttl}
    }
    
    proc obtener(in c: CacheTTL<K, V>, in k: K, out res: V) {
        requiere {k in c.datos &&L now() - c.tiempos_agregado[k] < c.ttl}
        asegura {res == c.datos[k]}
    }
    
    proc borrar(inout c: CacheTTL<K, V>, in k: K) {
        requiere {c == old(c) && k in c.datos}
        asegura {c.datos == delKey(old(c).datos, k) && c.tiempos_agregado == delKey(old(c).tiempos_agregado, k) && c.ttl == old(c).ttl}
    }
}

3.b.
TAD Cola<T> {
    obs elems: seq<T>

    proc crear(out c: Cola<T>) {
        requiere {True}
        asegura {c.elems == []}
    }

    proc vacia(in c: Cola<T>, out res: bool) {
        requiere {True}
        asegura {res == True <==> c.elems == []}
    }

    proc encolar(inout c: Cola<T>, in e: T) {
        requiere {c == old(c)}
        asegura {c.elems == old(c).elems + [e]}
    }

    proc desencolar(inout c: Cola<T>, out res: T) {
        requiere {c == old(c) && |c.elems| > 0}
        asegura {c.elems == old(c).elems[1..|old(c).elems|] && res = old(c).elems[0]}
    }
}

TAD CacheFIFO<K, V> {
    obs datos: dict<K, V>
    obs orden_agregado: seq<K>
    obs max: int

    proc crear(in max_: int, out c: CacheFIFO<T>) {
        requiere {True}
        asegura {c.datos == {} && c.max == max_ && c.orden_agregado == []}
    }

    proc vacio(in c: CacheFIFO<T>, out res: bool) {
        requiere {True}
        asegura {res == True <==> c.datos == {}}
    }

    proc esta(in c: CacheFIFO<K, V>, in k: K) {
        requiere {True}
        asegura {res == True <==> k in c.datos}
    }

    proc definir(inout c: CacheFIFO<K, V>, in k: K, in v: V) {
        requiere {c == old(c) && !(k in c.datos)}
        asegura {
            (|old(c).datos| == c.max ==>L 
                c.datos == setKey(delKey(old(c).datos, old(c).orden_agregado[0]), k, v) &&
                c.orden_agregado == old(c).orden_agregado[1..|old(c).orden_agregado|] + [k]) &&
            (|old(c).datos| < c.max ==>L
                c.datos == setKey(old(c).datos, k, v) &&
                c.orden_agregado == old(c).orden_agregado + [k])
        }
        asegura {c.max == old(c).max}
    }

    proc obtener(in c: CacheFIFO<K, V>, in k: K, out res: V) {
        requiere {k in c.datos}
        asegura {res == c.datos[k]}
    }

    proc borrar(inout c: CacheFIFO<K, V>, in k: K) {
        requiere {c == old(c) && k in c.datos}
        asegura {
            c.datos == delKey(old(c).datos, k) && 
            c.tiempos_agregado == 
                old(c).tiempos_agregado[0..indice(old(c).tiempos_agregado, k)] + 
                old(c).tiempos_agregado[indice(old(c).tiempos_agregado, k)+1..|old(c).tiempos_agregado|] &&
            c.max == old(c).max
        }
    }

    aux indice(s: seq<K>, k: K): int = sum i: int :: 0 <= i < |s| :: if s[i] == k then i else 0
}

3.c.
TAD CacheLRU<K, V> {
    obs datos: dict<K, V>
    obs accedido: dict<K, real>
    obs max: int

    proc crear(in max_: int, out c: CacheLRU<T>) {
        requiere {True}
        asegura {c.datos == {} && c.accedido == {} && c.max == max_}
    }

    proc esta(in c: CacheLRU<K, V>, in k: K) {
        requiere {True}
        asegura {res == True <==> k in c.datos}
    }

    proc obtener(inout c: CacheLRU<K, V>, in k: K, out res: V) {
        requiere {k in c.datos}
        asegura {res == c.datos[k]}
        asegura {c.accedido == setKey(old(c).accedido, k, now())}
        asegura {c.max == old(c).max && c.datos == old(c).datos}
    }

    proc borrar(inout c: CacheLRU<K, V>, in k: K) {
        asegura {c.datos == delKey(old(c).datos, k)}
        asegura {c.accedido == delKey(old(c).accedido, k)}
        asegura {c.max == old(c).max}
    }

    proc definir(inout c: CacheLRU<K, V>, in k: K k, in v: V) {
        asegura {|c.datos| < c.max ==> c.datos == setKey(old(c).datos, k, v)}
        asegura {
            |c.datos| == c.max ==> (
                (k in c.datos &&L c.datos[k] == v) &&
                (exists k_: K :: k_ in old(c).datos &&L (esMin(old(c).accedido, k_) && !(k_ in c.datos))) &&
                (forall k_: K :: (k_ in old(c).datos &&L !esMin(old(c).accedido, k_)) ==>L (k_ in c.datos &&L c.datos[k_] == old(c).datos[k_])) &&
                (forall k_: K :: k_ in c.datos ==>L (k_ in old(c).datos || k_ == k))
            )
        }
        asegura {c.accedido == setKey(old(c).accedido, k, now())}
        asegura {c.max == old(c).max}
    }

    pred esMin(d: dict<K, real>, k: K) {
        forall k_: K :: k_ in d ==>L d[k] <= d[k_]
    }
}

4.a.
TAD Pila<T> {
    obs elems: dict<int, T> /* indice, elem */
    obs info: dict<seq<char>, int> /* cantidad de elementos, expresada de esta manera para no observar con otra cosa que no sea un dict */

    proc crear(out p: Pila<T>) {
        requiere {True}
        asegura {p.elems = {}}
        asegura {p.info = {"cantidad": 0}}
    }

    proc vacia(in p: Pila<T>, out res: bool) {
        requiere {True}
        asegura {res == True <==> p.info["cantidad"] == 0}
    }

    proc apilar(inout c: Pila<T>, in e: T) {
        requiere {p == old(p)}
        asegura {p.elems == setKey(old(p).elems, old(p).info["cantidad"], e)}
        asegura {p.elems.info == setKey(old(p).info, "cantidad", old(p).info["cantidad"] + 1)}
    }

    proc desapilar(inout p: Pila<T>, out res: T) {
        requiere {p == old(p) && p.info["cantidad"] > 0}
        asegura {res == p.elems[p.info["cantidad"]]}
        asegura {p.elems == delKey(old(p).elems, p.info["cantidad"])}
        asegura {p.elems.info == setKey(old(p).info, "cantidad", old(p).info["cantidad"] - 1)}
    }
}

4.b.
TAD Diccionario<K, V> {
    obs pares: conj<tupla<K, V>>
    
    proc crear(out d: Diccionario<K, V>) {
        requiere {True}
        asegura {d.pares == {}}
    }

    proc acceder(in d: Diccionario<K, V>, in key: K, out res: V) {
        requiere {pertenece(d.pares, k)}
        asegura {<key, res> in d.pares}
    }

    proc agregar(inout d: Diccionario<K, V>, in key: K, in value: V) {
        requiere {d == old(d)}
        asegura {d.pares == old(d).pares + {<key, value>}}
    }

    proc quitar(inout d: Diccionario<K, V>, in key: K) {
        requiere {d == old(d)}
        asegura {d.pares == old(d).pares - {<key, value>}}
    }

    pred pertenece(d: Diccionario<K, V>, key: K) {
        exists v: V :: <key, v> in d.pares
    }
}

4.c.
TAD Punto {
    obs rho: real
    obs theta: real

    proc crear(in rho_, theta_: real, out p: Punto) {
        requiere {True}
        asegura {p.rho == rho_ && p.theta == theta_}
    }

    proc coordX(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.rho * cos(p.theta)}
    }

    proc coordY(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.rho * sin(p.theta)}
    }

    proc coordTheta(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.theta}
    }

    proc coordRho(in p: Punto, out res: real) {
        requiere {True}
        asegura {res == p.rho}
    }

    proc mover(inout p: Punto, in deltaX, deltaY: real) {
        requiere {p == old(p)}
        asegura {p.rho == sqrt((old(p).rho * cos(old(p).theta) + deltaX)**2 + (old(p).rho * sin(old(p).theta) + deltaY)**2)}
        asegura {p.theta == safearctan(old(p).rho * cos(old(p).theta) + deltaX, old(p).rho * sin(old(p).theta) + deltaY)}
    }

    proc escalar(inout p: Punto, in k: real) {
        requiere {p == old(p)}
        asegura {p.rho == k*old(p).rho && p.theta == old(p.theta)}
    }

    proc rotar(inout p: Punto, in a: real) {
        requiere {p == old(p)}
        asegura {p.rho == old(p).rho && p.theta == old(p.theta) + a}
    }

    aux safearctan(x, y: real): real = if x == 0 then signo(y)*pi/2 else arctan(y/x) fi
}

5.
/* asumo ejes cartesianos convencionales (x incrementa hacia la derecha, y incrementa hacia arriba) */
TAD Robot {
    obs pos: Coord
    obs historial: seq<Coord>
    info: Coord es struct<x: int, y: int>

    proc crear(out r: Robot) {
        requiere {True}
        asegura {r.pos = <x: 0, y: 0> && res.historial == [<x: 0, y: 0>]}
    }

    proc arriba(inout r: Robot) {
        requiere {r == old(r)}
        asegura {r.pos == <x: old(r).pos.x, y: old(r).pos.y + 1>}
        asegura {r.historial == old(r).historial + [r.pos]}
    }

    proc abajo(inout r: Robot) {
        requiere {r == old(r)}
        asegura {r.pos == <x: old(r).pos.x, y: old(r).pos.y - 1>}
        asegura {r.historial == old(r).historial + [r.pos]}
    }

    proc derecha(inout r: Robot) {
        requiere {r == old(r)}
        asegura {r.pos == <x: old(r).pos.x + 1, y: old(r).pos.y>}
        asegura {r.historial == old(r).historial + [r.pos]}
    }

    proc izquierda(inout r: Robot) {
        requiere {r == old(r)}
        asegura {r.pos == <x: old(r).pos.x - 1, y: old(r).pos.y>}
        asegura {r.historial == old(r).historial + [r.pos]}
    }

    proc posicion(in r: Robot, out res: Coord) {
        requiere {True}
        asegura {res == r.pos}
    }

    proc mas_derecha(in r: Robot, out c: Coord) { /* El enunciado es ambiguo sobre el tipo de retorno, prefiero devolver Coord */
        requiere {True}
        asegura {res in r.historial && forall i: int :: 0 <= i < |r.historial| ==>L res.x >= r.historial[i].x}
    }

    proc cuantas_veces_paso(in r: Robot, in c: Coord, out res: int) {
        requiere {True}
        asegura {res == #apariciones(r.historial, c)}
    }

    aux #apariciones(s: seq<T>, e: T): int = sum i: int :: 0 <= i < |s| :: if s[i] == e then 1 else 0 fi
}

6.
TAD Insoportables {
    obs famosos: conj<Famoso>
    obs enemigos: dict<Famoso, conj<Famoso>>
    info: Famoso es string (seq<char>)

    proc crear(out p: Insoportables) {
        requiere {True}
        asegura {p.famosos == {} && p.enemigos == {}}
    }

    proc nuevoFamoso(inout p: Insoportables, in f: Famoso) {
        requiere {p == old(p)}
        asegura {p.famosos == old(p).famosos + {f}}
        asegura {p.enemigos == setKey(old(p).enemigos, f, {})}        
    }

    proc peleados(in p: Insoportables, in f1: Famoso, in f2: Famoso, out res: bool) {
        requiere {True}
        asegura {f1 in p.famosos &&L f2 in p.enemigos[f1]}
    }
    
    proc pelear(inout p: Insoportables, in f1: Famoso, in f2: Famoso) {
        requiere {p == old(p) && f1 in p.famosos && f2 in p.famosos}
        asegura {p.enemigos[f1] == old(p).enemigos[f1] + {f2} && p.enemigos[f2] == old(p).enemigos[f2] + {f1}}
        asegura {forall f: Famoso :: f in old(p).enemigos && f != f1 && f != f2 ==>L p.enemigos[f] == old(p).enemigos[f]}
        asegura {forall f: Famoso :: !(f in old(p).enemigos) ==> !(f in p.enemigos)}
        asegura {p.famosos == old(p).famosos}
    }

    proc reconciliar(inout p: Insoportables, in f1: Famoso, in f2: Famoso) {
        requiere {p == old(p) && f1 in p.famosos && f2 in p.famosos}
        asegura {p.enemigos[f1] == old(p).enemigos[f1] - {f2} && p.enemigos[f2] == old(p).enemigos[f2] - {f1}}
        asegura {forall f: Famoso :: f in old(p).enemigos && f != f1 && f != f2 ==>L p.enemigos[f] == old(p).enemigos[f]}
        asegura {forall f: Famoso :: !(f in old(p).enemigos) ==> !(f in p.enemigos)}
        asegura {p.famosos == old(p).famosos}
    }

    proc masPeleadorHistorico(in p: Insoportables, out res: conj<Famoso>) {
        requiere {p.famosos != {}}
        asegura {exists fp: Famoso :: fp in p.enemigos && res == p.enemigos[fp] && forall f: Famoso :: f in p.famosos ==>L |res| >= |p.enemigos[f]|}
    }
}

7.
TAD Stock<T> {
    obs min: int
    obs productos: dict<Producto, int> /* {producto: cantidad en stock} */
    obs historial_compra: dict<Producto, seq<int>>
    obs historial_venta: dict<Producto, seq<int>>
    obs sustitutos: dict<Producto, Producto> /* producto sustituido: producto sustituto */
    info: Producto es T

    proc crear(in min_: int, out s: Stock) {
        requiere {min_ > 0}
        asegura {s.min == min_ && s.productos == {} && s.sustitutos == {} && s.historial_compra == {} && s.historial_venta == {}}
    }

    proc registrar_nuevo_producto(inout s: Stock, in p: Producto) {
        requiere {s == old(s) && !(p in s.productos)}
        asegura {s.productos == setKey(old(s).productos, p, s.min)}
        asegura {s.historial_compra == setKey(old(s).historial_compra, p, [s.min])}
        asegura {s.historial_venta == setKey(old(s).historial_venta, p, [])}
        asegura {s.sustitutos == old(s).sustitutos}
    }

    proc comprar_producto(inout s: Stock, in p: Producto, in q: int) {
        requiere {s == old(s) && p in s.productos}
        asegura {s.productos == setKey(old(s).productos, p, old(s).productos[p] + q)}
        asegura {s.historial_compra == setKey(old(s).historial_compra, p, old(s).historial_compra[p] + [q])}
        asegura {s.historial_venta == old(s).historial_venta}
        asegura {s.sustitutos == old(s).sustitutos}
    }

    proc vender_producto(inout s: Stock, in p: Producto, in q: int) {
        requiere {
            s == old(s) && p in s.productos &&L 
            (p in s.sustitutos ==> q <= s.productos[p] + s.productos[s.sustitutos[p]]) && (!(p in s.sustitutos) ==> q <= s.productos[p])
        }
        asegura {
            (q <= s.productos[p] ==>
                s.productos == setKey(old(s).productos, p, old(s).productos[p] - q) &&
                s.historial_venta == setKey(old(s).historial_venta, p, old(s).historial_venta[p] + [q])) &&
            (q > s.productos[p] ==>
                s.productos[p] == 0 && s.productos[psus] == old(s).productos[psus] - (q - old(s).productos[p]) &&
                s.historial_venta[p] == old(s).historial_venta[p] + old(s).productos[p] &&
                s.historial_venta[psus] == old(s).historial_venta[psus] + (q - old(s).productos[p]) &&
                (forall prod: Producto :: prod in old(s).productos && prod != p && prod != psus ==>L prod in s.productos && s.productos[prod] == old(s).productos[prod])
                (forall prod: Producto :: !(prod in old(s).productos) ==>L !(prod in s.productos)) &&
                (forall prod: Producto :: prod in old(s).historial_venta && prod != p && prod != psus ==>L prod in s.historial_venta && s.historial_venta[prod] == old(s).historial_venta[prod]) &&
                (forall prod: Producto :: !(prod in old(s).historial_venta) ==>L !(prod in s.historial_venta)))
        }
        asegura {s.historial_compra == old(s).historial_compra}
        asegura {s.sustitutos == old(s).sustitutos}
    }

    proc informar_sustituto(inout s: Stock, in p, psus: Producto) {
        requiere {s == old(s) && p in s.productos && psus in s.productos &&L no_es_sustituto_de_otro(s.sustitutos, p, psus)}
        asegura {s.sustitutos == setKey(old(s).sustitutos, p, psus)}
        asegura {s.productos == old(s).productos}
        asegura {s.historial_compra == old(s).historial_compra}
        asegura {s.historial_venta == old(s).historial_venta}
    }

    proc productos_escasos(in s: Stock, out res: conj<Producto>) {
        requiere {True}
        asegura {forall p: Producto :: p in s.productos &&L escaso(s, p) <==> p in res}
    }

    pred no_es_sustituto_de_otro(s: dict<Producto, Producto>, p, psus: Producto) {
        !(exists prod: Producto :: (prod in s && prod != p) &&L s[prod] == psus)
    }

    pred escaso(s: Stock, p: Producto) {
        s.sustitutos[p] == {} && s.productos[p] < s.min ||L
        p in s.sustitutos &&L (s.productos[s.sustitutos[p]] + s.productos[p]) < s.min
    }
}

8.
TAD Tablero {
    obs partida: Baldosa
    obs llegada: Baldosa
    obs saltos: dict<Baldosa, Baldosa> /* baldosa de origen: baldosa a la que se salta (si la celda no es "especial", el valor es igual a la clave) */
    info: Baldosa es int

    proc crear(in llegada_: Baldosa, in saltos_: dict<Baldosa, Baldosa>, out t: Tablero) {
        requiere {llegada_ > 6 && forall b: Baldosa :: b in saltos_ ==>L 0 <= b, saltos_[b] <= llegada_}
        asegura {t.partida == 0 && t.llegada == llegada_ && t.saltos == saltos_}
    }
}

/* asumo que las baldosas visitadas son sólo en las que un jugador estuvo al final de cada uno de sus turnos */
TAD Oca {
    obs tablero: Tablero
    obs posiciones: tupla<Baldosa, Baldosa> /* posición actual del juegador 0 y el jugador 1 */
    obs turno: int /* incrementa después de cada turno, cuando turno es par juega un jugador y cuando es impar juega el otro */
    obs historial_posiciones: tupla<seq<Baldosa>, seq<Baldosa>>
    obs historial_dados: tupla<seq<int>, seq<int>>
    info: Baldosa es int

    proc crear(in llegada_: Baldosa, in saltos_: dict<Baldosa, Baldosa>, out o: Oca) {
        requiere {llegada_ > 6 && forall b: Baldosa :: b in saltos_ ==>L 0 <= b, saltos_[b] <= llegada_}
        asegura {o.tablero.partida == 0 && o.tablero.llegada == llegada_ && o.tablero.saltos == saltos_}
        asegura {o.posiciones == <0, 0> && o.turno == 0 && o.historial_posiciones == <[], []> && o.historial_dados == <[], []>}
    }

    proc jugar_un_turno(inout o: Oca, in dado: int) {
        requiere {o == old(o) && && 1 <= dado <= 6 !hay_ganador(o)}
        asegura {
            (old(o).turno%2 == 0 ==>
                o.posiciones == <o.tablero.saltos[desplazamiento(dado, old(o).posiciones[0], o.tablero.llegada)], old(o).posiciones[1]>
                o.historial_posiciones == <old(o).historial_posiciones[0] + [posiciones[0]], old(o).historial_posiciones[1]>
                o.historial_dados == <old(o).historial_dados[0] + [dado], old(o).historial_dados[1]>) &&
            (old(o).turno%2 == 1 ==>
                o.posiciones == <old(o).posiciones[0], o.tablero.saltos[desplazamiento(dado, old(o).posiciones[1], o.tablero.llegada)]>
                o.historial_posiciones == <old(o).historial_posiciones[0], old(o).historial_posiciones[1] + [posiciones[1]]>
                o.historial_dados == <old(o).historial_dados[0], old(o).historial_dados[1] + [dado]>)
        }
        asegura {o.tablero == old(o).tablero}
        asegura {o.turno == old(o).turno + 1}
    }

    proc tiradas(in o: Oca, out res: tupla<seq<int>, seq<int>>) {
        requiere {True}
        asegura {res == o.historial_dados}
    }

    proc baldosa_visitada(in o: Oca, in j: int, in baldosa: Baldosa, out res: bool) {
        requiere {j == 0 || j == 1}
        asegura {res == baldosa in o.historial_posiciones[j]}
    }

    pred hay_ganador(o: Oca) {
        o.posiciones[0] == o.tablero.llegada || o.posiciones[1] == o.tablero.llegada
    }

    aux desplazamiento(dado, pos, max: int) = if dado + pos <= max then dado + pos else 2*max - (dado + pos)
}

9.
TAD Persona {
    obs dni: int
    obs tipo: seq<char> /* "bien" o "prole" */

    proc crear(in dni_: int, in tipo_: seq<char>, out p: Persona) {
        requiere {tipo_ == "bien" || tipo_ == "prole"}
        asegura {p.dni == dni_ && p.tipo == tipo_}
    }
}

TAD BancoClasista {
    obs cola_bien: seq<Persona>
    obs cola_prole: seq<Persona>
    obs caja_A_libre: bool
    obs caja_B_libre: bool

    proc crear(out b: BancoClasista) {
        requiere {True}
        asegura {b.cola_bien == [] && b.cola_prole == [] && b.caja_A_libre == True && b.caja_B_libre == True}
    }

    proc encolar(inout b: BancoClasista, in p: Persona) {
        requiere {b == old(b) && !(exists p_cola: Persona :: (p_cola in b.cola_bien || p_cola in b.cola_prole) && p_cola.dni == p.dni)}
        asegura {
            (p.tipo == "bien" ==>
                b.cola_bien == old(b).cola_bien + [p] &&
                b.cola_prole == old(b).cola_prole) &&
            (p.tipo == "prole" ==>
                b.cola_prole == old(b).cola_prole + [p] &&
                b.cola_bien == old(b).cola_bien)
        }
        asegura {b.caja_A_libre == old(b).caja_A_libre && b.caja_B_libre == old(b).caja_B_libre}
    }

    proc abandonar_cola(inout b: BancoClasista, in p: Persona) {
        requiere {b == old(b) && (p in b.cola_bien || p in b.cola_prole)}
        asegura {
            (p in old(b).cola_bien ==>
                b.cola_bien == old(b).cola_bien[0..indice(old(b).cola_bien, p)] + old(b).cola_bien[indice(old(b).cola_bien, p)+1..|old(b).cola_bien|] &&
                b.cola_prole == old(b).cola_prole) &&
            (!(p in old(b).cola_bien) && p in old(b).cola_prole ==>
                b.cola_prole == old(b).cola_prole[0..indice(old(b).cola_prole, p)] + old(b).cola_prole[indice(old(b).cola_prole, p)+1..|old(b).cola_prole|] &&
                b.cola_bien == old(b).cola_bien)
        }
        asegura {b.caja_A_libre == old(b).caja_A_libre && b.caja_B_libre == old(b).caja_B_libre}
    }

    proc liberar_caja_A(inout b: BancoClasista) {
        requiere {b == old(b)}
        asegura {b.caja_A_libre == True}
        asegura {b.cola_bien == old(b).cola_bien && b.cola_prole == old(b).cola_prole && b.caja_B_libre == old(b).caja_B_libre}
    }

    proc liberar_caja_B(inout b: BancoClasista) {
        requiere {b == old(b)}
        asegura {b.caja_B_libre == True}
        asegura {b.cola_bien == old(b).cola_bien && b.cola_prole == old(b).cola_prole && b.caja_A_libre == old(b).caja_A_libre}
    }

    proc desencolar_bien(inout b: BancoClasista) {
        requiere {b == old(b) && (b.caja_A_libre == True || b.caja_B_libre == True) && b.cola_bien != []}
        asegura {
            (old(b).caja_A_libre == True ==>
                b.caja_A_libre == False && b.cola_bien == old(b).cola_bien[1..|old(b).cola_bien|] &&
                b.caja_B_libre == old(b).caja_B_libre && b.cola_prole == old(b).cola_prole) &&
            (!old(b).caja_A_libre && old(b).caja_B_libre ==>
                b.caja_B_libre == False && b.cola_prole == old(b).cola_bien[1..|old(b).cola_bien|] &&
                b.caja_A_libre == False && b.cola_prole == old(b).cola_prole)
        }
        asegura {b.caja_B_libre == old(b).caja_B_libre && b.cola_prole == old(b).cola_prole}
    }

    proc desencolar_prole(inout b: BancoClasista) {
        requiere {b == old(b) && b.caja_B_libre == True && b.cola_prole != [] && b.cola_bien == []}
        asegura {b.caja_B_libre == False && b.cola_prole == old(b).cola_prole[1..|old(b).cola_prole|]}
        asegura {b.caja_A_libre == old(b).caja_A_libre && b.cola_bien == old(b).cola_bien}
    }

    aux indice(cola: seq<Persona>, p: Persona): int = sum i: int :: 0 <= i < |cola| &&L cola[i] == p :: i
}

10.
TAD ColaBañoExamen {
    obs alumnos: conj<Alumno>
    obs veces_baño: dict<Alumno, int>
    obs cola: seq<Alumno>
    obs alumno_en_baño: seq<Alumno>
    obs max_baño: int
    info: Alumno es int (dni)

    proc crear(in max_baño_: int, in alumnos_: conj<Alumno> out c: ColaBañoExamen) {
        requiere {max_baño_ > 0}
        asegura {c.alumnos == alumnos_ && c.cola == [] && c.alumno_en_baño == [] && c.max_baño == max_baño_}
        asegura {forall a: Alumno :: a in c.veces_baño <==> a in alumnos_}
        asegura {forall a: Alumno :: a in c.veces_baño ==>L c.veces_baño[a] == 0}
    }

    proc encolar(inout c: ColaBañoExamen, in a: Alumno) {
        requiere {c == old(c) && a in c.alumnos &&L c.veces_baño[a] <= c.max_baño && !(a in c.cola)}
        asegura {c.cola == old(c).cola + [a]}
        asegura {c.alumnos == old(c).alumnos && c.veces_baño == old(c).veces_baño && c.alumno_en_baño == old(c).alumno_en_baño && c.max_baño == old(c).max_baño}        
    }

    proc abandonar_cola(inout c: ColaBañoExamen, in a: Alumno) { 
        requiere {c == old(c) && a in c.cola}
        asegura {old(c).cola[0..indice(old(c).cola, a)] + old(c).cola[indice(old(c).cola, a)+1..|old(c).cola|]}
        asegura {c.alumnos == old(c).alumnos && c.veces_baño == old(c).veces_baño && c.alumno_en_baño == old(c).alumno_en_baño && c.max_baño == old(c).max_baño}  
    }

    proc regresar_del_baño_y_desencolar(inout c: ColaBañoExamen) { /* acoplados para garantizar el caracter "automático" y no permitir comportamientos prohibidos por la especificación informal del problema - en este caso, que en un momento dado el baño esté vacío y la cola no */
        requiere {c == old(c)}
        asegura {
            (old(c).cola != [] ==>
                c.veces_baño == setKey(old(c).veces_baño, old(c).cola[0], old(c).veces_baño[old(c).cola[0]] + 1) &&
                c.alumno_en_baño == [old(c).cola[0]] &&
                c.cola == old(c).cola[1..|old(c).cola|]) &&
            (old(c).cola == [] ==>
                c.veces_baño == old(c).veces_baño &&
                c.alumno_en_baño == [] &&
                c.cola == [])
        }
        asegura {c.alumnos == old(c).alumnos && c.max_baño == old(c).max_baño}
    }

    aux indice(cola: seq<Alumno>, a: Alumno): int = sum i: int :: 0 <= i < |cola| &&L cola[i] == a :: i
}

11.
TAD EmpresaTaD {
    obs tecnicos_disp: int
    obs tecnicos_asig: int
    obs pendientes: seq<Domicilio>
    info: Domicilio es seq<char> (identificador único del domicilio)

    proc crear(in tecnicos_disp_: int, out e: EmpresaTaD) {
        requiere {tecnicos_disp > 0}
        asegura {e.tecnicos_disp == tecnicos_disp_ && e.tecnicos_asig == 0 && e.pendientes == []}
    }

    proc recibir_procesar_pedido(inout e: EmpresaTaD, in d: Domicilio) {
        requiere {e == old(e)}
        asegura {
            (old(e).tecnicos_disp > 0 ==>
                e.tecnicos_disp == old(e).tecnicos_disp - 1 && e.tecnicos_asig == old(e).tecnicos_asig + 1 && e.pendientes == old(e).pendientes) &&
            (old(e).tecnicos_disp == 0 ==>
                e.tecnicos_disp == 0 && e.tecnicos_asig == old(e).tecnicos_asig && e.pendientes == old(e).pendientes + [d])
        }
    }

    proc resolver_problema_redirigir_tecnico(inout e: EmpresaTaD) {
        requiere {e == old(e)}
        asegura {
            (old(e).pendientes != [] ==>
                e.pendientes == old(e).pendientes[1..|old(e).pendientes|] &&
                e.tecnicos_disp == old(e).tecnicos_disp && e.tecnicos_asig == old(e).tecnicos_asig) &&
            (old(e).pendientes == [] ==>
                e.pendientes == [] &&
                e.tecnicos_disp == old(e).tecnicos_disp + 1 && e.tecnicos_asig == old(e).tecnicos_asig - 1)
        }
    }
}