Heap_H — Min-heap como subtipo de BTree (with HIDE)

1. Especificación

-- ============================================================
-- Heap_H — Especificación de min-heap como subtipo de BTree.
--
-- Constructores básicos (lo que el cliente puede usar):
--   * Heap_Empty   (renombrado de BTree_Empty, heredado de BTree)
--   * Heap_Insert  (propio de Heap_H)
--
-- BTree_Create queda OCULTO mediante HIDE: el cliente solo
-- puede construir heaps componiendo Heap_Empty y Heap_Insert.
-- Esto garantiza por construcción la propiedad de heap (la
-- raíz es siempre menor o igual que todos los descendientes).
--
-- Representación interna: skew heap. Tanto la inserción como
-- la fusión intercambian los subárboles izquierdo y derecho
-- en cada nivel, dando complejidad amortizada O(log n) sin
-- necesidad de balanceo explícito.
--
-- Heap_Merge es una operación auxiliar oculta, usada por
-- Heap_DeleteMin para fusionar los dos subárboles tras
-- eliminar la raíz.
-- ============================================================

CLASS Heap_H [Element : WithOrder]
IS-SUBTYPE-OF BTree[Element]
  rename BTree_Empty as Heap_Empty
BASIC CONSTRUCTORS Heap_Empty, Heap_Insert
EFFECTIVE

OPERATIONS

  -- Renombrado heredado de BTree.
  Heap_Empty: -> Heap_H;

  -- Constructor propio: inserción que preserva la propiedad de heap.
  Heap_Insert: Heap_H(h) * Element(e) -> Heap_H;

  -- Observación: el mínimo, que vive siempre en la raíz.
  Heap_Min: Heap_H(h) -> Element
      pre: not BTree_IsEmpty(h);

  -- Eliminar el mínimo (la raíz).
  Heap_DeleteMin: Heap_H(h) -> Heap_H
      pre: not BTree_IsEmpty(h);

  -- Operación auxiliar: fusionar dos heaps (skew merge).
  -- Se oculta junto con BTree_Create.
  Heap_Merge: Heap_H(h1) * Heap_H(h2) -> Heap_H;

AXIOMS  h, h1, h2, L, R, L1, L2, R1, R2: Heap_H;  x, x1, x2, i: Element;

  -- ──────────────────────────────────────────────────────
  -- Heap_Insert: inserción al estilo skew heap, reescrita a
  -- términos con BTree_Create (forma canónica interna).
  -- ──────────────────────────────────────────────────────

  -- Caso base: insertar en heap vacío produce un singleton.
  Heap_Insert(Heap_Empty() as Heap_H, i) =
      BTree_Create(Heap_Empty() as Heap_H,
                   Heap_Empty() as Heap_H,
                   i) as Heap_H;

  -- Caso i < raíz: i pasa a ser la nueva raíz; el heap viejo
  -- queda íntegro como subárbol izquierdo, el derecho vacío.
  -- Se respeta la propiedad de heap: i ≤ todos los descendientes.
  (i < x) implies
  Heap_Insert(BTree_Create(L, R, x) as Heap_H, i) =
      BTree_Create(BTree_Create(L, R, x) as Heap_H,
                   Heap_Empty() as Heap_H,
                   i) as Heap_H;

  -- Caso i ≥ raíz: la raíz x permanece; i se inserta
  -- recursivamente en el subárbol derecho R, y luego se
  -- intercambian los subárboles (skew) para balance amortizado.
  not (i < x) implies
  Heap_Insert(BTree_Create(L, R, x) as Heap_H, i) =
      BTree_Create(Heap_Insert(R as Heap_H, i), L, x) as Heap_H;

  -- ──────────────────────────────────────────────────────
  -- Heap_Min: el mínimo siempre está en la raíz.
  -- ──────────────────────────────────────────────────────
  Heap_Min(BTree_Create(L, R, x) as Heap_H) = x;

  -- ──────────────────────────────────────────────────────
  -- Heap_DeleteMin: eliminar la raíz, fusionar L y R.
  -- ──────────────────────────────────────────────────────
  Heap_DeleteMin(BTree_Create(L, R, x) as Heap_H) =
      Heap_Merge(L as Heap_H, R as Heap_H);

  -- ──────────────────────────────────────────────────────
  -- Heap_Merge (skew merge): fusionar dos heaps preservando
  -- la propiedad de heap, con intercambio de subárboles en
  -- cada nivel recursivo.
  -- ──────────────────────────────────────────────────────

  -- Identidades: fusionar con vacío deja el otro intacto.
  Heap_Merge(Heap_Empty() as Heap_H, h) = h;
  Heap_Merge(h, Heap_Empty() as Heap_H) = h;

  -- Recursivo: el de raíz menor queda arriba; su subárbol
  -- derecho se mergea con el otro heap entero; los subárboles
  -- izquierdo y derecho se intercambian (skew).

  (x1 < x2) implies
  Heap_Merge(BTree_Create(L1, R1, x1) as Heap_H,
             BTree_Create(L2, R2, x2) as Heap_H) =
      BTree_Create(
          Heap_Merge(R1 as Heap_H, BTree_Create(L2, R2, x2) as Heap_H),
          L1,
          x1
      ) as Heap_H;

  not (x1 < x2) implies
  Heap_Merge(BTree_Create(L1, R1, x1) as Heap_H,
             BTree_Create(L2, R2, x2) as Heap_H) =
      BTree_Create(
          Heap_Merge(BTree_Create(L1, R1, x1) as Heap_H, R2 as Heap_H),
          L2,
          x2
      ) as Heap_H;

  -- ──────────────────────────────────────────────────────
  -- Encapsulamiento: ocultar la representación interna.
  -- El cliente solo dispone de Heap_Empty y Heap_Insert
  -- como constructores; BTree_Create y Heap_Merge son
  -- detalles de implementación.
  -- ──────────────────────────────────────────────────────
  HIDE BTree_Create, Heap_Merge

END-CLASS

2. Estructura de los axiomas por operación

3. Ejemplo: inserción sucesiva 5, 3, 7, 1

Trazando los axiomas de Heap_Insert paso a paso:

En cada paso la raíz es el mínimo. El paso "Insert 7" muestra el efecto del skew: como not (7 < 3), recursamos en R (que era vacío, así que 7 va como singleton) y luego intercambiamos: el R nuevo (con 7) pasa a la izquierda, y la L original (que tenía 5) pasa a la derecha.

4. Garantías