Especificaciones algebraicas completas 1 Universidad Nacional de Rio Negro - Sede Andina
Especificaciones Algebraicas completas para secuencias ¶ Objetivos observables ¶ Identificás el problema que modela el capítulo y el TAD/estructura más adecuada.
Justificás decisiones de diseño con costo temporal/espacial y contrato de operaciones.
Aplicás el contenido en Java sin romper invariantes ni contrato público.
Este capítulo cataloga las especificaciones algebraicas rigurosas de las estructuras de datos más utilizadas en programación. Cada especificación integra:
Sorts y Signatura: tipos abstractos y operaciones tipadas.
Generadores, Modificadores, Observadores: clasificación de operaciones.
Axiomas: ecuaciones que definen semántica.
Invariantes: propiedades que mantiene la estructura.
Contratos: precondiciones, postcondiciones, invariantes de representación.
Estas especificaciones son implementación-agnósticas : funcionan con arrays dinámicos, listas enlazadas, o cualquier representación que respete los axiomas.
Este capítulo construye sobre Introducción a Tipos de Datos Abstractos
TDA Array (Arreglo) ¶ Un arreglo es una secuencia estática de elementos de igual tipo, accesibles mediante índices enteros en rango [ 0 , n ) [0, n) [ 0 , n ) n n n
Sorts y Signatura ¶ Sorts: A r r a y , E l e m e n t , B o o l , N Generadores: empty : → A r r a y create : N → A r r a y (crea arreglo de tama n ˜ o fijo) Modificadores: set : A r r a y × N × E l e m e n t → A r r a y Observadores: get : A r r a y × N → E l e m e n t length : A r r a y → N eq : A r r a y × A r r a y → B o o l \begin{align}
\text{Sorts:} \quad & \mathtt{Array}, \mathtt{Element}, \mathtt{Bool}, \mathbb{N} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{Array} \\
\quad & \text{create} : \mathbb{N} \to \mathtt{Array} \quad \text{(crea arreglo de tamaño fijo)} \\
\\
\text{Modificadores:} \\
\quad & \text{set} : \mathtt{Array} \times \mathbb{N} \times \mathtt{Element} \to \mathtt{Array} \\
\\
\text{Observadores:} \\
\quad & \text{get} : \mathtt{Array} \times \mathbb{N} \to \mathtt{Element} \\
\quad & \text{length} : \mathtt{Array} \to \mathbb{N} \\
\quad & \text{eq} : \mathtt{Array} \times \mathtt{Array} \to \mathtt{Bool}
\end{align} Sorts: Generadores: Modificadores: Observadores: Array , Element , Bool , N empty :→ Array create : N → Array (crea arreglo de tama n ˜ o fijo) set : Array × N × Element → Array get : Array × N → Element length : Array → N eq : Array × Array → Bool Axiomas ¶ Axioma 1 (length de empty):
length ( empty ) = 0 \text{length}(\text{empty}) = 0 length ( empty ) = 0 Axioma 2 (length de create):
length ( create ( n ) ) = n ∀ n ∈ N \text{length}(\text{create}(n)) = n \quad \forall n \in \mathbb{N} length ( create ( n )) = n ∀ n ∈ N Axioma 3 (get de set con índice coincidente):
get ( set ( a , i , v ) , i ) = v ∀ a , i , v \text{get}(\text{set}(a, i, v), i) = v \quad \forall a, i, v get ( set ( a , i , v ) , i ) = v ∀ a , i , v Axioma 4 (get de set con índice distinto):
i ≠ j ⟹ get ( set ( a , i , v ) , j ) = get ( a , j ) i \neq j \implies \text{get}(\text{set}(a, i, v), j) = \text{get}(a, j) i = j ⟹ get ( set ( a , i , v ) , j ) = get ( a , j ) Axioma 5 (igualdad de arreglos):
eq ( a 1 , a 2 ) = true ⟺ length ( a 1 ) = length ( a 2 ) ∧ ∀ i < length ( a 1 ) , get ( a 1 , i ) = get ( a 2 , i ) \text{eq}(a_1, a_2) = \text{true} \iff \text{length}(a_1) = \text{length}(a_2) \land \forall i < \text{length}(a_1), \text{get}(a_1, i) = \text{get}(a_2, i) eq ( a 1 , a 2 ) = true ⟺ length ( a 1 ) = length ( a 2 ) ∧ ∀ i < length ( a 1 ) , get ( a 1 , i ) = get ( a 2 , i ) Invariante ¶ I ( Array ) : ∀ a , length ( a ) ≥ 0 ∧ ∀ i , 0 ≤ i < length ( a ) I(\text{Array}) : \forall a, \; \text{length}(a) \geq 0 \land \forall i, \; 0 \leq i < \text{length}(a) I ( Array ) : ∀ a , length ( a ) ≥ 0 ∧ ∀ i , 0 ≤ i < length ( a ) El tamaño es siempre no negativo y los índices válidos están en rango.
Contratos ¶ Operación Precondición Postcondición Complejidad create(n)ninguna length ( result ) = n \text{length}(\text{result}) = n length ( result ) = n O ( n ) O(n) O ( n ) O ( n ) O(n) O ( n ) set(a, i, v)0 ≤ i < length ( a ) 0 \leq i < \text{length}(a) 0 ≤ i < length ( a ) get ( result , i ) = v \text{get}(\text{result}, i) = v get ( result , i ) = v O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) get(a, i)0 ≤ i < length ( a ) 0 \leq i < \text{length}(a) 0 ≤ i < length ( a ) devuelve elemento en posición i i i O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 )
TDA Stack (Pila) ¶ Una pila es una secuencia dinámica LIFO (last-in, first-out). Solo el elemento superior es accesible.
Sorts y Signatura ¶ Sorts: S t a c k , E l e m e n t , B o o l Generadores: empty : → S t a c k Modificadores: push : S t a c k × E l e m e n t → S t a c k pop : S t a c k → S t a c k Observadores: top : S t a c k → E l e m e n t isEmpty : S t a c k → B o o l size : S t a c k → N \begin{align}
\text{Sorts:} \quad & \mathtt{Stack}, \mathtt{Element}, \mathtt{Bool} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{Stack} \\
\\
\text{Modificadores:} \\
\quad & \text{push} : \mathtt{Stack} \times \mathtt{Element} \to \mathtt{Stack} \\
\quad & \text{pop} : \mathtt{Stack} \to \mathtt{Stack} \\
\\
\text{Observadores:} \\
\quad & \text{top} : \mathtt{Stack} \to \mathtt{Element} \\
\quad & \text{isEmpty} : \mathtt{Stack} \to \mathtt{Bool} \\
\quad & \text{size} : \mathtt{Stack} \to \mathbb{N}
\end{align} Sorts: Generadores: Modificadores: Observadores: Stack , Element , Bool empty :→ Stack push : Stack × Element → Stack pop : Stack → Stack top : Stack → Element isEmpty : Stack → Bool size : Stack → N Axiomas ¶ Axioma 1 (pop de vacía):
pop ( empty ) = empty \text{pop}(\text{empty}) = \text{empty} pop ( empty ) = empty Axioma 2 (size vacía):
size ( empty ) = 0 \text{size}(\text{empty}) = 0 size ( empty ) = 0 Axioma 3 (isEmpty vacía):
isEmpty ( empty ) = true \text{isEmpty}(\text{empty}) = \text{true} isEmpty ( empty ) = true Axioma 4 (pop de push):
pop ( push ( s , e ) ) = s ∀ s ∈ S t a c k , e ∈ E l e m e n t \text{pop}(\text{push}(s, e)) = s \quad \forall s \in \mathtt{Stack}, e \in \mathtt{Element} pop ( push ( s , e )) = s ∀ s ∈ Stack , e ∈ Element Axioma 5 (top de push):
top ( push ( s , e ) ) = e \text{top}(\text{push}(s, e)) = e top ( push ( s , e )) = e Axioma 6 (isEmpty de push):
isEmpty ( push ( s , e ) ) = false \text{isEmpty}(\text{push}(s, e)) = \text{false} isEmpty ( push ( s , e )) = false Axioma 7 (size de push):
size ( push ( s , e ) ) = size ( s ) + 1 \text{size}(\text{push}(s, e)) = \text{size}(s) + 1 size ( push ( s , e )) = size ( s ) + 1 Invariante ¶ I ( Stack ) : ∀ s , size ( s ) ≥ 0 ∧ ( isEmpty ( s ) = true ⟺ size ( s ) = 0 ) I(\text{Stack}) : \forall s, \; \text{size}(s) \geq 0 \land (\text{isEmpty}(s) = \text{true} \iff \text{size}(s) = 0) I ( Stack ) : ∀ s , size ( s ) ≥ 0 ∧ ( isEmpty ( s ) = true ⟺ size ( s ) = 0 ) El tamaño es no negativo y vacío es equivalente a tamaño cero.
Contratos ¶ Operación Precondición Postcondición Complejidad push(s, e)ninguna top ( result ) = e ∧ isEmpty ( result ) = false \text{top}(\text{result}) = e \land \text{isEmpty}(\text{result}) = \text{false} top ( result ) = e ∧ isEmpty ( result ) = false O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) pop(s)ninguna (falla gracefully si vacía) si isEmpty ( s ) = true \text{isEmpty}(s) = \text{true} isEmpty ( s ) = true O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) top(s)isEmpty ( s ) = false \text{isEmpty}(s) = \text{false} isEmpty ( s ) = false devuelve elemento más reciente O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 )
TDA Queue (Cola) ¶ Una cola es una secuencia dinámica FIFO (first-in, first-out). Se agregan elementos al final; se retiran del frente.
Sorts y Signatura ¶ Sorts: Q u e u e , E l e m e n t , B o o l Generadores: empty : → Q u e u e Modificadores: enqueue : Q u e u e × E l e m e n t → Q u e u e dequeue : Q u e u e → Q u e u e Observadores: front : Q u e u e → E l e m e n t isEmpty : Q u e u e → B o o l size : Q u e u e → N \begin{align}
\text{Sorts:} \quad & \mathtt{Queue}, \mathtt{Element}, \mathtt{Bool} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{Queue} \\
\\
\text{Modificadores:} \\
\quad & \text{enqueue} : \mathtt{Queue} \times \mathtt{Element} \to \mathtt{Queue} \\
\quad & \text{dequeue} : \mathtt{Queue} \to \mathtt{Queue} \\
\\
\text{Observadores:} \\
\quad & \text{front} : \mathtt{Queue} \to \mathtt{Element} \\
\quad & \text{isEmpty} : \mathtt{Queue} \to \mathtt{Bool} \\
\quad & \text{size} : \mathtt{Queue} \to \mathbb{N}
\end{align} Sorts: Generadores: Modificadores: Observadores: Queue , Element , Bool empty :→ Queue enqueue : Queue × Element → Queue dequeue : Queue → Queue front : Queue → Element isEmpty : Queue → Bool size : Queue → N Axiomas ¶ Axioma 1 (dequeue de vacía):
dequeue ( empty ) = empty \text{dequeue}(\text{empty}) = \text{empty} dequeue ( empty ) = empty Axioma 2 (isEmpty vacía):
isEmpty ( empty ) = true \text{isEmpty}(\text{empty}) = \text{true} isEmpty ( empty ) = true Axioma 3 (enqueue-dequeue FIFO):
front ( enqueue ( empty , e ) ) = e \text{front}(\text{enqueue}(\text{empty}, e)) = e front ( enqueue ( empty , e )) = e Axioma 4 (dequeue preserva frente): Si la cola tiene múltiples elementos, dequeue lo retira:
dequeue ( enqueue ( q , e nuevo ) ) = q si isEmpty ( q ) = false \text{dequeue}(\text{enqueue}(q, e_{\text{nuevo}})) = q \quad \text{si } \text{isEmpty}(q) = \text{false} dequeue ( enqueue ( q , e nuevo )) = q si isEmpty ( q ) = false Axioma 5 (dequeue-enqueue conmutan casi):
dequeue ( enqueue ( q , e 1 ) ) = enqueue ( dequeue ( q ) , e 1 ) si isEmpty ( q ) = false \text{dequeue}(\text{enqueue}(q, e_1)) = \text{enqueue}(\text{dequeue}(q), e_1) \quad \text{si } \text{isEmpty}(q) = \text{false} dequeue ( enqueue ( q , e 1 )) = enqueue ( dequeue ( q ) , e 1 ) si isEmpty ( q ) = false Axioma 6 (isEmpty de enqueue):
isEmpty ( enqueue ( q , e ) ) = false \text{isEmpty}(\text{enqueue}(q, e)) = \text{false} isEmpty ( enqueue ( q , e )) = false Axioma 7 (size de enqueue):
size ( enqueue ( q , e ) ) = size ( q ) + 1 \text{size}(\text{enqueue}(q, e)) = \text{size}(q) + 1 size ( enqueue ( q , e )) = size ( q ) + 1 Invariante ¶ I ( Queue ) : ∀ q , size ( q ) ≥ 0 ∧ ( isEmpty ( q ) = true ⟺ size ( q ) = 0 ) I(\text{Queue}) : \forall q, \; \text{size}(q) \geq 0 \land (\text{isEmpty}(q) = \text{true} \iff \text{size}(q) = 0) I ( Queue ) : ∀ q , size ( q ) ≥ 0 ∧ ( isEmpty ( q ) = true ⟺ size ( q ) = 0 ) Contratos ¶ Operación Precondición Postcondición Complejidad enqueue(q, e)ninguna elemento agregado al final; isEmpty ( result ) = false \text{isEmpty}(\text{result}) = \text{false} isEmpty ( result ) = false O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) dequeue(q)ninguna si vacía, resultado = empty; sino, primer elemento removido O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) front(q)isEmpty ( q ) = false \text{isEmpty}(q) = \text{false} isEmpty ( q ) = false devuelve elemento al frente O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 )
TDA LinkedList (Lista Enlazada Simple) ¶ Una lista enlazada simple es una secuencia dinámica de nodos donde cada nodo referencia al siguiente. Permite inserción/remoción eficiente en cualquier posición conocida.
Sorts y Signatura ¶ Sorts: L i n k e d L i s t , E l e m e n t , N , B o o l Generadores: empty : → L i n k e d L i s t singleton : E l e m e n t → L i n k e d L i s t Modificadores: insertAt : L i n k e d L i s t × N × E l e m e n t → L i n k e d L i s t removeAt : L i n k e d L i s t × N → L i n k e d L i s t prepend : L i n k e d L i s t × E l e m e n t → L i n k e d L i s t append : L i n k e d L i s t × E l e m e n t → L i n k e d L i s t Observadores: get : L i n k e d L i s t × N → E l e m e n t size : L i n k e d L i s t → N isEmpty : L i n k e d L i s t → B o o l contains : L i n k e d L i s t × E l e m e n t → B o o l \begin{align}
\text{Sorts:} \quad & \mathtt{LinkedList}, \mathtt{Element}, \mathbb{N}, \mathtt{Bool} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{LinkedList} \\
\quad & \text{singleton} : \mathtt{Element} \to \mathtt{LinkedList} \\
\\
\text{Modificadores:} \\
\quad & \text{insertAt} : \mathtt{LinkedList} \times \mathbb{N} \times \mathtt{Element} \to \mathtt{LinkedList} \\
\quad & \text{removeAt} : \mathtt{LinkedList} \times \mathbb{N} \to \mathtt{LinkedList} \\
\quad & \text{prepend} : \mathtt{LinkedList} \times \mathtt{Element} \to \mathtt{LinkedList} \\
\quad & \text{append} : \mathtt{LinkedList} \times \mathtt{Element} \to \mathtt{LinkedList} \\
\\
\text{Observadores:} \\
\quad & \text{get} : \mathtt{LinkedList} \times \mathbb{N} \to \mathtt{Element} \\
\quad & \text{size} : \mathtt{LinkedList} \to \mathbb{N} \\
\quad & \text{isEmpty} : \mathtt{LinkedList} \to \mathtt{Bool} \\
\quad & \text{contains} : \mathtt{LinkedList} \times \mathtt{Element} \to \mathtt{Bool}
\end{align} Sorts: Generadores: Modificadores: Observadores: LinkedList , Element , N , Bool empty :→ LinkedList singleton : Element → LinkedList insertAt : LinkedList × N × Element → LinkedList removeAt : LinkedList × N → LinkedList prepend : LinkedList × Element → LinkedList append : LinkedList × Element → LinkedList get : LinkedList × N → Element size : LinkedList → N isEmpty : LinkedList → Bool contains : LinkedList × Element → Bool Axiomas ¶ Axioma 1 (isEmpty vacía):
isEmpty ( empty ) = true \text{isEmpty}(\text{empty}) = \text{true} isEmpty ( empty ) = true Axioma 2 (size vacía):
size ( empty ) = 0 \text{size}(\text{empty}) = 0 size ( empty ) = 0 Axioma 3 (prepend a vacía):
get ( prepend ( empty , e ) , 0 ) = e \text{get}(\text{prepend}(\text{empty}, e), 0) = e get ( prepend ( empty , e ) , 0 ) = e Axioma 4 (prepend desplaza índices):
get ( prepend ( l , e ) , i + 1 ) = get ( l , i ) ∀ i ≥ 0 \text{get}(\text{prepend}(l, e), i+1) = \text{get}(l, i) \quad \forall i \geq 0 get ( prepend ( l , e ) , i + 1 ) = get ( l , i ) ∀ i ≥ 0 Axioma 5 (append a vacía):
get ( append ( empty , e ) , 0 ) = e \text{get}(\text{append}(\text{empty}, e), 0) = e get ( append ( empty , e ) , 0 ) = e Axioma 6 (size de prepend):
size ( prepend ( l , e ) ) = size ( l ) + 1 \text{size}(\text{prepend}(l, e)) = \text{size}(l) + 1 size ( prepend ( l , e )) = size ( l ) + 1 Axioma 7 (removeAt índice válido):
size ( removeAt ( l , i ) ) = size ( l ) − 1 si 0 ≤ i < size ( l ) \text{size}(\text{removeAt}(l, i)) = \text{size}(l) - 1 \quad \text{si } 0 \leq i < \text{size}(l) size ( removeAt ( l , i )) = size ( l ) − 1 si 0 ≤ i < size ( l ) Axioma 8 (removeAt preserva otros elementos):
j < i ⟹ get ( removeAt ( l , i ) , j ) = get ( l , j ) j < i \implies \text{get}(\text{removeAt}(l, i), j) = \text{get}(l, j) j < i ⟹ get ( removeAt ( l , i ) , j ) = get ( l , j )
j ≥ i ∧ j < size ( l ) − 1 ⟹ get ( removeAt ( l , i ) , j ) = get ( l , j + 1 ) j \geq i \land j < \text{size}(l) - 1 \implies \text{get}(\text{removeAt}(l, i), j) = \text{get}(l, j+1) j ≥ i ∧ j < size ( l ) − 1 ⟹ get ( removeAt ( l , i ) , j ) = get ( l , j + 1 ) Invariante ¶ I ( LinkedList ) : ∀ l , size ( l ) ≥ 0 ∧ ( isEmpty ( l ) = true ⟺ size ( l ) = 0 ) ∧ no circular references I(\text{LinkedList}) : \forall l, \; \text{size}(l) \geq 0 \land (\text{isEmpty}(l) = \text{true} \iff \text{size}(l) = 0) \land \text{no circular references} I ( LinkedList ) : ∀ l , size ( l ) ≥ 0 ∧ ( isEmpty ( l ) = true ⟺ size ( l ) = 0 ) ∧ no circular references Contratos ¶ Operación Precondición Postcondición Complejidad insertAt(l, i, e)0 ≤ i ≤ size ( l ) 0 \leq i \leq \text{size}(l) 0 ≤ i ≤ size ( l ) elemento insertado en posición i i i O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) removeAt(l, i)0 ≤ i < size ( l ) 0 \leq i < \text{size}(l) 0 ≤ i < size ( l ) elemento removido; elementos posteriores se desplazan O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) get(l, i)0 ≤ i < size ( l ) 0 \leq i < \text{size}(l) 0 ≤ i < size ( l ) devuelve elemento en posición i i i O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) prepend(l, e)ninguna elemento agregado al inicio O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) append(l, e)ninguna elemento agregado al final O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 )
TDA DoublyLinkedList (Lista Enlazada Doble) ¶ Una lista enlazada doble permite navegación bidireccional. Cada nodo referencia al siguiente y al anterior.
Sorts y Signatura ¶ Sorts: D o u b l y L i n k e d L i s t , E l e m e n t , N , B o o l Generadores: empty : → D o u b l y L i n k e d L i s t Modificadores: insertAt : D o u b l y L i n k e d L i s t × N × E l e m e n t → D o u b l y L i n k e d L i s t removeAt : D o u b l y L i n k e d L i s t × N → D o u b l y L i n k e d L i s t prepend : D o u b l y L i n k e d L i s t × E l e m e n t → D o u b l y L i n k e d L i s t append : D o u b l y L i n k e d L i s t × E l e m e n t → D o u b l y L i n k e d L i s t Observadores: get : D o u b l y L i n k e d L i s t × N → E l e m e n t getFromEnd : D o u b l y L i n k e d L i s t × N → E l e m e n t (desde el final) size : D o u b l y L i n k e d L i s t → N isEmpty : D o u b l y L i n k e d L i s t → B o o l \begin{align}
\text{Sorts:} \quad & \mathtt{DoublyLinkedList}, \mathtt{Element}, \mathbb{N}, \mathtt{Bool} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{DoublyLinkedList} \\
\\
\text{Modificadores:} \\
\quad & \text{insertAt} : \mathtt{DoublyLinkedList} \times \mathbb{N} \times \mathtt{Element} \to \mathtt{DoublyLinkedList} \\
\quad & \text{removeAt} : \mathtt{DoublyLinkedList} \times \mathbb{N} \to \mathtt{DoublyLinkedList} \\
\quad & \text{prepend} : \mathtt{DoublyLinkedList} \times \mathtt{Element} \to \mathtt{DoublyLinkedList} \\
\quad & \text{append} : \mathtt{DoublyLinkedList} \times \mathtt{Element} \to \mathtt{DoublyLinkedList} \\
\\
\text{Observadores:} \\
\quad & \text{get} : \mathtt{DoublyLinkedList} \times \mathbb{N} \to \mathtt{Element} \\
\quad & \text{getFromEnd} : \mathtt{DoublyLinkedList} \times \mathbb{N} \to \mathtt{Element} \quad \text{(desde el final)} \\
\quad & \text{size} : \mathtt{DoublyLinkedList} \to \mathbb{N} \\
\quad & \text{isEmpty} : \mathtt{DoublyLinkedList} \to \mathtt{Bool}
\end{align} Sorts: Generadores: Modificadores: Observadores: DoublyLinkedList , Element , N , Bool empty :→ DoublyLinkedList insertAt : DoublyLinkedList × N × Element → DoublyLinkedList removeAt : DoublyLinkedList × N → DoublyLinkedList prepend : DoublyLinkedList × Element → DoublyLinkedList append : DoublyLinkedList × Element → DoublyLinkedList get : DoublyLinkedList × N → Element getFromEnd : DoublyLinkedList × N → Element (desde el final) size : DoublyLinkedList → N isEmpty : DoublyLinkedList → Bool Axiomas (adicionales a los de LinkedList) ¶ Axioma 1 (navegación bidireccional):
getFromEnd ( l , i ) = get ( l , size ( l ) − 1 − i ) ∀ i < size ( l ) \text{getFromEnd}(l, i) = \text{get}(l, \text{size}(l) - 1 - i) \quad \forall i < \text{size}(l) getFromEnd ( l , i ) = get ( l , size ( l ) − 1 − i ) ∀ i < size ( l ) Axioma 2 (get es consistente en ambas direcciones):
get ( l , i ) = getFromEnd ( l , size ( l ) − 1 − i ) \text{get}(l, i) = \text{getFromEnd}(l, \text{size}(l) - 1 - i) get ( l , i ) = getFromEnd ( l , size ( l ) − 1 − i ) Axioma 3 (prepend refleja en navegación desde fin):
getFromEnd ( prepend ( l , e ) , 0 ) = get ( l , size ( l ) − 1 ) si isEmpty ( l ) = false \text{getFromEnd}(\text{prepend}(l, e), 0) = \text{get}(l, \text{size}(l) - 1) \quad \text{si } \text{isEmpty}(l) = \text{false} getFromEnd ( prepend ( l , e ) , 0 ) = get ( l , size ( l ) − 1 ) si isEmpty ( l ) = false Invariante (extendida) ¶ I ( DoublyLinkedList ) : LinkedList invariants ∧ ∀ i , next [ prev [ i ] ] = i ∧ prev [ next [ i ] ] = i I(\text{DoublyLinkedList}) : \text{LinkedList invariants} \land \forall i, \; \text{next}[\text{prev}[i]] = i \land \text{prev}[\text{next}[i]] = i I ( DoublyLinkedList ) : LinkedList invariants ∧ ∀ i , next [ prev [ i ]] = i ∧ prev [ next [ i ]] = i Cada nodo tiene referencias bidireccionales consistentes.
Contratos ¶ Operación Precondición Postcondición Complejidad insertAt(l, i, e)0 ≤ i ≤ size ( l ) 0 \leq i \leq \text{size}(l) 0 ≤ i ≤ size ( l ) elemento insertado en posición i i i O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) removeAt(l, i)0 ≤ i < size ( l ) 0 \leq i < \text{size}(l) 0 ≤ i < size ( l ) elemento removido O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) get(l, i)0 ≤ i < size ( l ) 0 \leq i < \text{size}(l) 0 ≤ i < size ( l ) devuelve elemento en posición i i i O ( min ( i , n − i ) ) O(\min(i, n-i)) O ( min ( i , n − i )) O ( 1 ) O(1) O ( 1 ) getFromEnd(l, i)0 ≤ i < size ( l ) 0 \leq i < \text{size}(l) 0 ≤ i < size ( l ) devuelve elemento desde el final O ( min ( i , n − i ) ) O(\min(i, n-i)) O ( min ( i , n − i )) O ( 1 ) O(1) O ( 1 ) prepend(l, e)ninguna elemento agregado al inicio O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 ) append(l, e)ninguna elemento agregado al final O ( 1 ) O(1) O ( 1 ) O ( 1 ) O(1) O ( 1 )
TDA CircularLinkedList (Lista Enlazada Circular) ¶ Una lista enlazada circular es una secuencia donde el último nodo referencia al primero, formando un ciclo cerrado.
Sorts y Signatura ¶ Sorts: C i r c u l a r L i n k e d L i s t , E l e m e n t , N , B o o l Generadores: empty : → C i r c u l a r L i n k e d L i s t Modificadores: insertAt : C i r c u l a r L i n k e d L i s t × N × E l e m e n t → C i r c u l a r L i n k e d L i s t removeAt : C i r c u l a r L i n k e d L i s t × N → C i r c u l a r L i n k e d L i s t rotate : C i r c u l a r L i n k e d L i s t × N → C i r c u l a r L i n k e d L i s t Observadores: get : C i r c u l a r L i n k e d L i s t × N → E l e m e n t size : C i r c u l a r L i n k e d L i s t → N isEmpty : C i r c u l a r L i n k e d L i s t → B o o l \begin{align}
\text{Sorts:} \quad & \mathtt{CircularLinkedList}, \mathtt{Element}, \mathbb{N}, \mathtt{Bool} \\
\\
\text{Generadores:} \\
\quad & \text{empty} : \to \mathtt{CircularLinkedList} \\
\\
\text{Modificadores:} \\
\quad & \text{insertAt} : \mathtt{CircularLinkedList} \times \mathbb{N} \times \mathtt{Element} \to \mathtt{CircularLinkedList} \\
\quad & \text{removeAt} : \mathtt{CircularLinkedList} \times \mathbb{N} \to \mathtt{CircularLinkedList} \\
\quad & \text{rotate} : \mathtt{CircularLinkedList} \times \mathbb{N} \to \mathtt{CircularLinkedList} \\
\\
\text{Observadores:} \\
\quad & \text{get} : \mathtt{CircularLinkedList} \times \mathbb{N} \to \mathtt{Element} \\
\quad & \text{size} : \mathtt{CircularLinkedList} \to \mathbb{N} \\
\quad & \text{isEmpty} : \mathtt{CircularLinkedList} \to \mathtt{Bool}
\end{align} Sorts: Generadores: Modificadores: Observadores: CircularLinkedList , Element , N , Bool empty :→ CircularLinkedList insertAt : CircularLinkedList × N × Element → CircularLinkedList removeAt : CircularLinkedList × N → CircularLinkedList rotate : CircularLinkedList × N → CircularLinkedList get : CircularLinkedList × N → Element size : CircularLinkedList → N isEmpty : CircularLinkedList → Bool Axiomas ¶ Axioma 1 (circularidad: acceso modular):
get ( l , i ) = get ( l , i m o d size ( l ) ) ∀ i ≥ size ( l ) \text{get}(l, i) = \text{get}(l, i \bmod \text{size}(l)) \quad \forall i \geq \text{size}(l) get ( l , i ) = get ( l , i mod size ( l )) ∀ i ≥ size ( l ) (Los índices se envuelven circularmente.)
Axioma 2 (rotación preserva elementos):
size ( rotate ( l , k ) ) = size ( l ) \text{size}(\text{rotate}(l, k)) = \text{size}(l) size ( rotate ( l , k )) = size ( l )
get ( rotate ( l , k ) , i ) = get ( l , ( i + k ) m o d size ( l ) ) \text{get}(\text{rotate}(l, k), i) = \text{get}(l, (i + k) \bmod \text{size}(l)) get ( rotate ( l , k ) , i ) = get ( l , ( i + k ) mod size ( l )) Axioma 3 (isEmpty vacía):
isEmpty ( empty ) = true \text{isEmpty}(\text{empty}) = \text{true} isEmpty ( empty ) = true Axioma 4 (removeAt en lista circular):
size ( removeAt ( l , i ) ) = size ( l ) − 1 si isEmpty ( l ) = false \text{size}(\text{removeAt}(l, i)) = \text{size}(l) - 1 \quad \text{si } \text{isEmpty}(l) = \text{false} size ( removeAt ( l , i )) = size ( l ) − 1 si isEmpty ( l ) = false Invariante ¶ I ( CircularLinkedList ) : u ˊ ltimo nodo → primer nodo ∧ sin terminaci o ˊ n nula I(\text{CircularLinkedList}) : \text{último nodo} \to \text{primer nodo} \land \text{sin terminación nula} I ( CircularLinkedList ) : u ˊ ltimo nodo → primer nodo ∧ sin terminaci o ˊ n nula Todos los nodos están conectados en un ciclo cerrado.
Contratos ¶ Operación Precondición Postcondición Complejidad rotate(l, k)ninguna orden cíclico rotado k k k O ( k ) O(k) O ( k ) O ( 1 ) O(1) O ( 1 ) get(l, i)ninguna (índices envolventes) devuelve elemento; i m o d size i \bmod \text{size} i mod size i ≥ size i \geq \text{size} i ≥ size O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) insertAt(l, i, e)ninguna elemento insertado; ciclo preservado O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 ) removeAt(l, i)isEmpty ( l ) = false \text{isEmpty}(l) = \text{false} isEmpty ( l ) = false elemento removido; ciclo preservado O ( n ) O(n) O ( n ) O ( 1 ) O(1) O ( 1 )
Comparativa: Propiedades Algebraicas y Complejidad ¶ TDA Acceso Inserción Remoción Iteración Complejidad Típica Invariante clave Array O(1) directo Estática Estática Lineal Acceso O(1), modificación O(1) Tamaño fijo Stack LIFO Final Final LIFO push/pop/top O(1) Vacía ↔ size = 0 Queue FIFO Final Inicio FIFO enqueue/dequeue/front O(1) FIFO order LinkedList O(n) Cualquier Cualquier Unidireccional get O(n), insert/remove O(n) No circular DoublyLinkedList O(n) Cualquier Cualquier Bidireccional get O(min(i,n-i)), insert/remove O(n) Refs. simétricas CircularLinkedList O(n) Cualquier Cualquier Cíclica get O(n), rotate O(k), insert/remove O(n) Ciclo cerrado
Validación: Demostración de Axiomas ¶ Ejemplo: Stack ¶ Proposición: Para toda pila s s s e e e
isEmpty ( pop ( push ( s , e ) ) ) = isEmpty ( s ) \text{isEmpty}(\text{pop}(\text{push}(s, e))) = \text{isEmpty}(s) isEmpty ( pop ( push ( s , e ))) = isEmpty ( s ) Demostración por inducción:
Base: s = empty s = \text{empty} s = empty
isEmpty ( pop ( push ( empty , e ) ) ) = isEmpty ( empty ) (Axioma 4: pop de push) = true (Axioma 3) = isEmpty ( empty ) (hip o ˊ tesis) \begin{align}
\text{isEmpty}(\text{pop}(\text{push}(\text{empty}, e)))
&= \text{isEmpty}(\text{empty}) && \text{(Axioma 4: pop de push)} \\
&= \text{true} && \text{(Axioma 3)} \\
&= \text{isEmpty}(\text{empty}) && \text{(hipótesis)}
\end{align} isEmpty ( pop ( push ( empty , e ))) = isEmpty ( empty ) = true = isEmpty ( empty ) (Axioma 4: pop de push) (Axioma 3) (hip o ˊ tesis) Paso inductivo: Asumimos isEmpty ( pop ( push ( s , e ) ) ) = isEmpty ( s ) \text{isEmpty}(\text{pop}(\text{push}(s, e))) = \text{isEmpty}(s) isEmpty ( pop ( push ( s , e ))) = isEmpty ( s ) s s s
Para s ′ = push ( s , e ′ ) s' = \text{push}(s, e') s ′ = push ( s , e ′ )
isEmpty ( pop ( push ( push ( s , e ′ ) , e ) ) ) = isEmpty ( push ( s , e ′ ) ) (Axioma 4) = isEmpty ( s ′ ) (definici o ˊ n) \begin{align}
\text{isEmpty}(\text{pop}(\text{push}(\text{push}(s, e'), e)))
&= \text{isEmpty}(\text{push}(s, e')) && \text{(Axioma 4)} \\
&= \text{isEmpty}(s') && \text{(definición)}
\end{align} isEmpty ( pop ( push ( push ( s , e ′ ) , e ))) = isEmpty ( push ( s , e ′ )) = isEmpty ( s ′ ) (Axioma 4) (definici o ˊ n) Por inducción, la proposición vale. ∎
Ejemplo: LinkedList ¶ Proposición: Para lista l l l i i i e e e
get ( removeAt ( insertAt ( l , i , e ) , i ) , i ) ≠ e \text{get}(\text{removeAt}(\text{insertAt}(l, i, e), i), i) \neq e get ( removeAt ( insertAt ( l , i , e ) , i ) , i ) = e (Insertar y luego remover en el mismo lugar restaura la lista original.)
Esta proposición se valida por análisis de casos sobre la estructura de la lista, similar a la demostración de stack.
Resumen ¶ Las especificaciones algebraicas de estructuras de datos fundamentales proporcionan:
Precisión formal: Cada operación tiene axiomas que gobiernan su comportamiento.
Independencia de implementación: Los axiomas no prescriben cómo implementar, solo qué garantizar.
Verificabilidad: Los axiomas se convierten directamente en tests unitarios.
Composicionalidad: Operaciones correctas se componen en programas correctos.
Estas especificaciones son el cimiento sobre el cual se construyen implementaciones seguras, testables y reemplazables en cualquier lenguaje de programación.
Próximo paso ¶ Una vez que comprendés las especificaciones algebraicas completas de estructuras fundamentales, el siguiente paso es implementarlas en Java respetando los contratos algebraicos. Esto significa escribir código que satisfaga todos los axiomas, con tests que validen cada axioma para garantizar que la implementación es correcta.
Ejercicios de verificación ¶ Resolvé un caso mínimo usando la estructura/algoritmo del capítulo y documentá por qué esa elección es válida.
Construí un contraejemplo donde una elección alternativa falle (rendimiento o corrección).
Escribí una prueba corta en Java que verifique un invariante crítico.