Traducción "fiel" de la especificación algebraica: misma jerarquía (BSTree IS-SUBTYPE-OF BTree), mismos nombres de operaciones, misma inmutabilidad observacional, mismas precondiciones.
Resumen del paquete: dos archivos de cabecera C++ (BTree.hpp y BSTree.hpp) más un main.cpp que ejercita las trazas ya documentadas. La implementación respeta cuatro principios traídos del spec algebraico:
Inmutabilidad observacional — todas las operaciones son const y devuelven nuevas instancias.
Sharing estructural — los subárboles se almacenan vía std::shared_ptr<const Node>: cada Insert/Delete crea O(log n) nodos nuevos y reutiliza el resto.
Encapsulamiento — la "ascensión" de un BTree a BSTree es un constructor privado de BSTree: refleja la cláusula HIDE BTree_Create.
Precondiciones declaradas — cada operación parcial chequea su pre: y lanza std::logic_error si se viola.
1. Filosofía de diseño — correspondencia spec ↔ código
Construcción Nereus
Traducción C++
CLASS BTree [elem]
template <typename Elem> class BTree
BASIC CONSTRUCTORS BTree_Empty, BTree_Create
Dos métodos estáticos: BTree::BTree_Empty() y BTree::BTree_Create(L, R, v); representación interna con std::shared_ptr<const Node> (nullptr = empty).
CLASS BSTree [Element:WithOrder]
template <typename Element> class BSTree. La restricción WithOrder se asume vía operator<, operator>, operator== en Element.
IS-SUBTYPE-OF BTree[Element]
class BSTree : public BTree<Element> (herencia pública).
HIDE BTree_Create
El constructor BSTree(const BTree<Element>&) está marcado private. Solo los métodos de BSTree pueden "ascender" un BTree a BSTree: el cliente no puede saltearse BSTree_Insert para violar la invariante BST.
Axiomas equacionales (cada uno define un caso del operador)
Implementación recursiva que sigue la estructura del axioma: if (isEmpty) → caso base; else compara raíz y recurre.
Precondiciones pre: ...
throw std::logic_error al violarlas, antes de cualquier modificación.
Inmutabilidad implícita (axiomas dan rewriting, no mutación)
Métodos const; valores de retorno por valor; nodos const dentro de shared_ptr.
Recursivo: matchea el axioma (e=e1) or belongs(t1) or belongs(t2).
BSTree (hereda todo lo de arriba)
BSTree_Insertpre: not belongs(e, t)
BSTree BSTree_Insert(const Element& e) const
Implementa el caso base + 2 reglas recursivas.
BSTree_Deletepre: belongs(e, t)
BSTree BSTree_Delete(const Element& e) const
Implementa los 6 casos A–F.
BSTree_Minpre: not isEmpty(t)
Element BSTree_Min() const
Recursión por la izquierda.
Auxiliares C++ agregadas (no en spec, sirven para inspección)
—
int size() const
Cantidad de nodos. Necesaria para los cout del demo.
—
std::string toString() const
Recorrido in-order como [a, b, c, ...].
—
std::string prettyPrint() const
Dibujo del árbol con líneas ├── / └──.
3. Especificación Nereus
-- ============================================================
-- BSTree — Especificación con constructores básicos
-- BTree_Empty (heredado) y BSTree_Insert (propio).
--
-- Encapsulamiento: BTree_Create se OCULTA con la cláusula HIDE
-- para que la API pública de BSTree exponga solo los dos
-- constructores básicos (BTree_Empty y BSTree_Insert) y las
-- operaciones derivadas.
-- ============================================================
CLASS BTree [elem]
BASIC CONSTRUCTORS BTree_Empty, BTree_Create
EFFECTIVE
TYPE BTree
OPERATIONS
BTree_Empty: -> BTree;
BTree_Create: BTree * BTree * elem -> BTree;
BTree_IsEmpty: BTree -> Boolean;
BTree_Root: BTree(t) -> elem pre: not BTree_IsEmpty(t);
BTree_Left: BTree(t) -> BTree pre: not BTree_IsEmpty(t);
BTree_Right: BTree(t) -> BTree pre: not BTree_IsEmpty(t);
belongs: elem * BTree -> Boolean;
AXIOMS t1, t2: BTree; e, e1: elem;
BTree_IsEmpty(BTree_Empty()) = True;
BTree_IsEmpty(BTree_Create(t1, t2, e)) = False;
BTree_Root (BTree_Create(t1, t2, e)) = e;
BTree_Left (BTree_Create(t1, t2, e)) = t1;
BTree_Right (BTree_Create(t1, t2, e)) = t2;
belongs(e, BTree_Empty()) = False;
belongs(e, BTree_Create(t1, t2, e1)) =
(e = e1) or (belongs(e, t1) or belongs(e, t2));
END-CLASS
CLASS BSTree [Element: WithOrder]
IS-SUBTYPE-OF BTree[Element]
BASIC CONSTRUCTORS BTree_Empty, BSTree_Insert
EFFECTIVE
OPERATIONS
BSTree_Insert: BSTree(t) * Element(e) -> BSTree
pre: not belongs(e, t);
BSTree_Delete: BSTree(t) * Element(e) -> BSTree
pre: belongs(e, t);
BSTree_Min: BSTree(t) -> Element
pre: not BTree_IsEmpty(t);
AXIOMS b, b1, b2: BSTree; i, j: Element;
BSTree_Insert(BTree_Empty() as BSTree, i) =
BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, i) as BSTree;
(i < j) implies
BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
BTree_Create(BSTree_Insert(b1 as BSTree, i), b2, j) as BSTree;
(i > j) implies
BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
BTree_Create(b1, BSTree_Insert(b2 as BSTree, i), j) as BSTree;
BTree_IsEmpty(b1) implies
BSTree_Min(BTree_Create(b1, b2, i) as BSTree) = i;
not BTree_IsEmpty(b1) implies
BSTree_Min(BTree_Create(b1, b2, i) as BSTree) = BSTree_Min(b1 as BSTree);
-- Caso A: j < i, recurrir en el subárbol izquierdo.
(j < i) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
BTree_Create(BSTree_Delete(b1 as BSTree, j), b2, i) as BSTree;
-- Caso B: j > i, recurrir en el subárbol derecho.
(j > i) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
BTree_Create(b1, BSTree_Delete(b2 as BSTree, j), i) as BSTree;
-- Caso C: j = i y ambos vacíos -> resultado vacío.
(j = i and BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
BTree_Empty() as BSTree;
-- Caso D: j = i, solo derecho no vacío -> derecho.
(j = i and BTree_IsEmpty(b1) and not BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) = b2 as BSTree;
-- Caso E: j = i, solo izquierdo no vacío -> izquierdo.
(j = i and not BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) = b1 as BSTree;
-- Caso F: j = i, ambos no vacíos -> reemplazar raíz por
-- el mínimo del subárbol derecho, y borrar ese mínimo.
(j = i and not BTree_IsEmpty(b1) and not BTree_IsEmpty(b2)) implies
BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
BTree_Create(
b1,
BSTree_Delete(b2 as BSTree, BSTree_Min(b2 as BSTree)),
BSTree_Min(b2 as BSTree)
) as BSTree;
HIDE BTree_Create
END-CLASS
# Con g++ (Linux/macOS/WSL/MinGW):
cd cpp
g++ -std=c++17 -O2 -Wall main.cpp -o bstree_demo
./bstree_demo
# Con clang++:
clang++ -std=c++17 -O2 -Wall main.cpp -o bstree_demo
# Con MSVC (Visual Studio Developer Command Prompt):
cl /std:c++17 /EHsc /W4 main.cpp /Fe:bstree_demo.exe
bstree_demo.exe
# Con el Makefile incluido:
cd cpp
make run
Sobre HIDE y la herencia pública: en Nereus, HIDE BTree_Create dice "el cliente no puede llamar a BTree_Create sobre un BSTree". En C++ optamos por hacer privado el constructor de ascensiónBSTree(const BTree&), en lugar de cambiar la visibilidad de BTree_Create (que sigue siendo público en BTree — un BTree "puro" sí lo necesita). Esto es semánticamente equivalente: cualquier BTree_Create que un cliente arme será de tipo BTree, no BSTree, y no se puede convertir al subtipo. La invariante BST queda garantizada por construcción.
Sobre el sharing estructural: al hacer t.BSTree_Insert(8) sobre un árbol de 100 nodos, solo se crean ~7 nuevos Node (log₂ 100). El árbol original sigue intacto y los subárboles no tocados se reutilizan a través de los shared_ptr. Esto es lo que da la persistencia "barata" típica de las estructuras funcionales — pagás O(log n) por cada Insert/Delete tanto en tiempo como en memoria adicional, no O(n).