Otras dos asignaturas

1 files changed, 1680 insertions, 0 deletions

diff --git a/aed1/n1.lyx b/aed1/n1.lyx
new file mode 100644
index 0000000..d39e26b
--- /dev/null
+++ b/aed1/n1.lyx
@@ -0,0 +1,1680 @@
+#LyX 2.3 created this file. For more info see http://www.lyx.org/
+\lyxformat 544
+\begin_document
+\begin_header
+\save_transient_properties true
+\origin unavailable
+\textclass book
+\use_default_options true
+\maintain_unincluded_children false
+\language spanish
+\language_package default
+\inputencoding auto
+\fontencoding global
+\font_roman "default" "default"
+\font_sans "default" "default"
+\font_typewriter "default" "default"
+\font_math "auto" "auto"
+\font_default_family default
+\use_non_tex_fonts false
+\font_sc false
+\font_osf false
+\font_sf_scale 100 100
+\font_tt_scale 100 100
+\use_microtype false
+\use_dash_ligatures true
+\graphics default
+\default_output_format default
+\output_sync 0
+\bibtex_command default
+\index_command default
+\paperfontsize default
+\spacing single
+\use_hyperref false
+\papersize default
+\use_geometry false
+\use_package amsmath 1
+\use_package amssymb 1
+\use_package cancel 1
+\use_package esint 1
+\use_package mathdots 1
+\use_package mathtools 1
+\use_package mhchem 1
+\use_package stackrel 1
+\use_package stmaryrd 1
+\use_package undertilde 1
+\cite_engine basic
+\cite_engine_type default
+\biblio_style plain
+\use_bibtopic false
+\use_indices false
+\paperorientation portrait
+\suppress_date false
+\justification true
+\use_refstyle 1
+\use_minted 0
+\index Index
+\shortcut idx
+\color #008000
+\end_index
+\secnumdepth 3
+\tocdepth 3
+\paragraph_separation indent
+\paragraph_indentation default
+\is_math_indent 0
+\math_numbering_side default
+\quotes_style french
+\dynamic_quotes 0
+\papercolumns 1
+\papersides 1
+\paperpagestyle default
+\tracking_changes false
+\output_changes false
+\html_math_output 0
+\html_css_as_file 0
+\html_be_strict false
+\end_header
+
+\begin_body
+
+\begin_layout Standard
+Una 
+\series bold
+abstracción
+\series default
+ consiste en dejar a un lado lo irrelevante y centrarse en lo importante.
+ Distinguimos 
+\series bold
+niveles de abstracción
+\series default
+ según el nivel de detalle.
+ El 
+\series bold
+diseño mediante abs
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+trac
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+cio
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+nes
+\series default
+ consiste en identificar los subproblemas de cierto problema, especificar
+ cada uno de forma abstracta, resolverlos de forma separada, unir las soluciones
+ y verificar la solución para el problema original.
+ Esto se hace de forma recursiva.
+\end_layout
+
+\begin_layout Standard
+Junto con el concepto de abstracción viene el de 
+\series bold
+especificación
+\series default
+ de dicha abstracción.
+\end_layout
+
+\begin_layout Standard
+
+\series bold
+Mecanismos de abstracción
+\series default
+:
+\end_layout
+
+\begin_layout Itemize
+
+\series bold
+Por especificación
+\series default
+: Nos quedamos con la descripción del efecto o resultado, in
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+de
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+pen
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+dien
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+te
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+men
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+-
+\end_layout
+
+\end_inset
+
+te de cómo calcularlo (
+\series bold
+principio de ocultación de la implementación
+\series default
+).
+ Da lugar a la 
+\series bold
+encapsulación
+\series default
+, agrupar un conjunto de operaciones o tipos relacionados en un mismo módulo
+ o paquete.
+\end_layout
+
+\begin_layout Itemize
+
+\series bold
+Por parametrización
+\series default
+: El significado de la abstracción no es fijo, sino que depende de parámetros.
+ En la 
+\series bold
+parametrización de tipo
+\series default
+, el parámetro es un tipo de datos.
+\end_layout
+
+\begin_layout Section
+Especificaciones informales
+\end_layout
+
+\begin_layout Standard
+Una 
+\series bold
+especificación
+\series default
+ es la descripción de una abstracción, bien textualmente mediante el lenguaje
+ natural (especificación 
+\series bold
+informal
+\series default
+) o bien con una notación precisa de las propiedades de la abstracción (especifi
+cación 
+\series bold
+formal
+\series default
+), mediante una 
+\series bold
+notación
+\series default
+.
+ A continuación vemos los tipos de abstracciones y una notación propuesta
+ para su especificación informal.
+\end_layout
+
+\begin_layout Itemize
+
+\series bold
+Funcionales
+\series default
+: Abstraemos un trozo de código en una 
+\series bold
+rutina
+\series default
+, 
+\series bold
+procedimiento
+\series default
+ o 
+\series bold
+función
+\series default
+, al que asignamos un nombre.
+ Su especificación indica los parámetros de entrada, los de salida y el
+ efecto que tendrá su ejecución.
+\begin_inset Newline newline
+\end_inset
+
+
+\begin_inset Tabular
+<lyxtabular version="3" rows="2" columns="1">
+<features tabularvalignment="middle">
+<column alignment="left" valignment="top" width="90text%">
+<row>
+<cell alignment="left" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Especificación informal
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+Operación
+\series default
+ 
+\emph on
+nombre
+\emph default
+ 
+\family default
+[
+\family sans
+[
+\emph on
+T
+\emph default
+,
+\family default
+...
+\family sans
+:
+\emph on
+TipoDeTipo
+\emph default
+; 
+\family default
+...
+\family sans
+]
+\family default
+]
+\family sans
+ (
+\family default
+[
+\family sans
+\series bold
+ent
+\series default
+ 
+\emph on
+v1
+\emph default
+, 
+\family default
+...
+\family sans
+:
+\emph on
+Tipo
+\emph default
+1; 
+\emph on
+vn
+\emph default
+, 
+\family default
+...
+\family sans
+:
+\emph on
+Tipo2
+\emph default
+; 
+\family default
+...[
+\family sans
+;
+\family default
+]]
+\family sans
+ 
+\family default
+[
+\family sans
+\series bold
+sal
+\series default
+ 
+\emph on
+tipoResultado
+\family default
+\emph default
+]
+\family sans
+)
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\series bold
+Require:
+\series default
+ 
+\emph on
+Opcional, requisitos y restricciones de uso de la operación.
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\series bold
+Modifica:
+\series default
+ 
+\emph on
+Opcional, lista de parámetros de entrada que pueden ser
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+modificados.
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\series bold
+Calcula:
+\series default
+ 
+\emph on
+Descripción del resultado de la operación.
+\end_layout
+
+\end_inset
+</cell>
+</row>
+</lyxtabular>
+
+\end_inset
+
+
+\begin_inset Newline newline
+\end_inset
+
+Donde el 
+\family sans
+\emph on
+TipoDeTipo
+\family default
+\emph default
+ suele ser 
+\family sans
+tipo
+\family default
+.
+ Tanto en la especificación informal como en el pseudocódigo, los tipos
+ tanto de los parámetros de tipo como los propios de la función pueden depender
+ de parámetros anteriores.
+\end_layout
+
+\begin_layout Itemize
+
+\series bold
+De datos
+\series default
+: Se abstrae un dominio de valores, junto con operaciones sobre ese dominio
+ con 
+\series bold
+ocultación de la implementación
+\series default
+, en un 
+\series bold
+tipo abstracto de datos
+\series default
+ (
+\series bold
+TAD
+\series default
+).
+ Un 
+\series bold
+tipo contenedor
+\series default
+ es un TAD compuesto por un número arbitrario de valores de otro tipo.
+ Generalmente están 
+\series bold
+parametrizados
+\series default
+: dependen de un parámetro que indica el tipo de objetos almacenados.
+\begin_inset Newline newline
+\end_inset
+
+
+\begin_inset Tabular
+<lyxtabular version="3" rows="2" columns="1">
+<features tabularvalignment="middle">
+<column alignment="left" valignment="top" width="90text%">
+<row>
+<cell alignment="left" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Especificación informal
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+TAD
+\series default
+ 
+\emph on
+nombre
+\emph default
+ 
+\series bold
+es
+\series default
+ 
+\emph on
+listaDeOperaciones
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+Descripción
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+Descripción del significado, comportamiento y modo de uso del TAD.
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+Operaciones
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+Especificación informal de cada operación de la lista, según el punto anterior.
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+Fin
+\series default
+ 
+\emph on
+nombre
+\emph default
+.
+\end_layout
+
+\end_inset
+</cell>
+</row>
+</lyxtabular>
+
+\end_inset
+
+
+\begin_inset Newline newline
+\end_inset
+
+Así, un 
+\series bold
+tipo de datos
+\series default
+ es un concepto de implementación que debe ajustarse al comportamiento de
+ un TAD, y una 
+\series bold
+estructura de datos
+\series default
+ es la disposición en memoria de estos datos.
+\end_layout
+
+\begin_layout Itemize
+
+\series bold
+De iteradores
+\series default
+: Permiten realizar un recorrido de forma abstracta sobre los elementos
+ de una colección.
+ La especificación informal puede ser:
+\end_layout
+
+\begin_deeper
+\begin_layout Itemize
+Similar a la de una abstracción funcional, cambiando 
+\family sans
+\series bold
+Operación
+\family default
+\series default
+ por 
+\family sans
+\series bold
+Iterador
+\family default
+\series default
+ y añadiendo un parámetro de entrada de tipo 
+\family sans
+Operacion
+\family default
+.
+ La función puede devolver un valor si, por ejemplo, el iterador filtra
+ una colección de valores de un cierto tipo.
+\end_layout
+
+\begin_layout Itemize
+Similar a la de un TAD, cambiando 
+\family sans
+\series bold
+TAD
+\family default
+\series default
+ por 
+\family sans
+\series bold
+TipoIterador
+\family default
+\series default
+ y añadiendo operaciones como 
+\family sans
+Iniciar
+\family default
+, 
+\family sans
+Actual
+\family default
+, 
+\family sans
+Avanzar
+\family default
+ y 
+\family sans
+EsUltimo
+\family default
+.
+\end_layout
+
+\end_deeper
+\begin_layout Standard
+La abstracción en lenguajes de programación generalmente consiste en ofrecer
+ características más próximas al concepto teórico de TAD.
+ Los lenguajes primitivos como Fortran o BASIC ofrecían un conjunto predefinido
+ de tipos elementales, pero no permitían definir nuevos tipos, con lo que
+ el programador debía definir y manejar las variables adecuadas de forma
+ manual.
+ Posteriormente, lenguajes como C y Pascal permiten agrupar un conjunto
+ de variables bajo un mismo nombre, aunque no hay ocultación.
+ Los módulos o paquetes permiten agrupar bajo un mismo nombre una serie
+ de tipos y operaciones relacionados, y en algunos casos como en Modula-2,
+ estos ofrecen ocultación de la implementación: los tipos definidos en un
+ módulo sólo se pueden usar a través de las operaciones de este.
+\end_layout
+
+\begin_layout Standard
+Finalmente, en la programación orientada a objetos surge el concepto de
+ clase, que es al mismo tiempo un tipo definido por el usuario y un módulo
+ donde se encapsulan sus datos y operaciones, y soportan ocultación.
+ Un objeto es una instancia de una clase.
+ El 
+\series bold
+principio de acceso uniforme
+\series default
+ consiste en que los atributos y operaciones de una clase están conceptualmente
+ al mismo nivel, y se accede con 
+\family typewriter
+\emph on
+objeto
+\emph default
+.
+\emph on
+atributo
+\family default
+\emph default
+ u 
+\family typewriter
+\emph on
+objeto
+\emph default
+.
+\emph on
+operación
+\emph default
+(
+\family default
+...
+\family typewriter
+)
+\family default
+.
+ Algunos lenguajes orientados a objetos permiten parametrización de tipo,
+ dando lugar a TAD genéricos o parametrizados.
+\end_layout
+
+\begin_layout Standard
+Una implementación es 
+\series bold
+robusta
+\series default
+ si se autoprotege de valores inconsistentes de entrada, bien lanzando una
+ excepción o mediante programación por contrato, en la que el usuario se
+ compromete, de forma comprobable, a no pasar un valor inconsistente según
+ la especificación de la función.
+ 
+\end_layout
+
+\begin_layout Section
+Especificaciones formales
+\end_layout
+
+\begin_layout Standard
+Una 
+\series bold
+especificación formal
+\series default
+ define un TAD u operación de forma precisa, permitiendo la verificación
+ automática y formal de la corrección del programa y el uso de la especificación
+ en distintos ámbitos.
+ Estas especificaciones pueden llegar a ser ejecutables.
+ Distinguimos entre el 
+\series bold
+método axiomático
+\series default
+ o 
+\series bold
+algebraico
+\series default
+, que establece el significado de las operaciones de forma implícita mediante
+ 
+\series bold
+axiomas
+\series default
+ que especifican sus relaciones, y el 
+\series bold
+método constructivo
+\series default
+ u 
+\series bold
+operacional
+\series default
+, en el que cada operación se define por sí misma con significado explícito.
+\end_layout
+
+\begin_layout Standard
+Veremos un método constructivo al que llamaremos método axiomático, y que
+ escribimos en lenguaje Maude, describiendo un TAD del siguiente modo:
+\end_layout
+
+\begin_layout Standard
+\align center
+\begin_inset Tabular
+<lyxtabular version="3" rows="6" columns="2">
+<features tabularvalignment="middle">
+<column alignment="left" valignment="top" width="45text%">
+<column alignment="left" valignment="top" width="45text%">
+<row>
+<cell alignment="left" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Especificación formal
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="left" valignment="top" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+Maude
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+NOMBRE
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+NombreTAD
+\family default
+\emph default
+ [
+\family sans
+[
+\emph on
+T1
+\emph default
+,
+\family default
+...
+\family sans
+]
+\family default
+]
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family typewriter
+\series bold
+fmod
+\series default
+ 
+\emph on
+NOMBRETAD
+\emph default
+ 
+\series bold
+is
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+CONJUNTOS
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+CONJ
+\emph default
+
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+Descripción
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+protecting 
+\emph on
+TADIMPORTADO
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+sort 
+\emph on
+CONJ
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+subsort 
+\emph on
+A
+\emph default
+ < 
+\emph on
+B
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+SINTAXIS
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family sans
+\emph on
+operación
+\emph default
+:
+\family default
+ [
+\family sans
+\emph on
+conjPar1
+\family default
+\emph default
+
+\begin_inset Formula $\times$
+\end_inset
+
+...]
+\family sans
+ 
+\begin_inset Formula $\rightarrow$
+\end_inset
+
+ 
+\emph on
+conjResultado
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+op 
+\emph on
+operación
+\emph default
+ : 
+\family default
+[
+\family typewriter
+\emph on
+conjPar11
+\emph default
+ 
+\begin_inset Formula $\times$
+\end_inset
+
+ ...
+\family default
+]
+\family typewriter
+ -> 
+\emph on
+conjResultado1
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+ops 
+\emph on
+op1
+\emph default
+ 
+\family default
+...
+
+\family typewriter
+ : 
+\family default
+[
+\family typewriter
+\emph on
+conjPar21
+\emph default
+ 
+\begin_inset Formula $\times$
+\end_inset
+
+ ...
+\family default
+]
+\family typewriter
+ -> 
+\emph on
+conjResultado2
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family sans
+\series bold
+SEMÁNTICA
+\end_layout
+
+\begin_layout Plain Layout
+\begin_inset Formula $\forall$
+\end_inset
+
+
+\family sans
+\emph on
+ var1
+\emph default
+, 
+\family default
+...
+
+\family sans
+ 
+\begin_inset Formula $\in$
+\end_inset
+
+
+\emph on
+ CONJ
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\emph on
+ExprA
+\emph default
+ = 
+\emph on
+ExprB
+\end_layout
+
+\begin_layout Plain Layout
+
+\family sans
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+var 
+\emph on
+v
+\emph default
+ : 
+\emph on
+CONJ
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+vars 
+\emph on
+v1
+\emph default
+ 
+\family default
+...
+
+\family typewriter
+ : 
+\emph on
+CONJ
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+eq 
+\emph on
+ExprA
+\emph default
+ = 
+\emph on
+ExprB
+\emph default
+ .
+\end_layout
+
+\begin_layout Plain Layout
+
+\family typewriter
+\begin_inset space \qquad{}
+\end_inset
+
+
+\family default
+...
+\end_layout
+
+\end_inset
+</cell>
+</row>
+<row>
+<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\end_layout
+
+\end_inset
+</cell>
+<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
+\begin_inset Text
+
+\begin_layout Plain Layout
+
+\family typewriter
+\series bold
+endfm
+\end_layout
+
+\end_inset
+</cell>
+</row>
+</lyxtabular>
+
+\end_inset
+
+
+\end_layout
+
+\begin_layout Standard
+El nombre de los conjuntos suele ser de una letra, y debe haber un conjunto
+ asociado al TAD, y si el TAD es genérico, uno para cada parámetro con el
+ mismo nombre dado en la sección anterior (
+\family sans
+\emph on
+T1
+\family default
+\emph default
+, etc.).
+ También, en la especificación se declaran conjuntos asociados a otros TADs
+ pero que se usan en este, mientras que en Maude se usa 
+\family typewriter
+protecting
+\family default
+ para importar todos los conjuntos, junto con sus operaciones, de otro TAD.
+ Para tipos finitos en la especificación, si en la 
+\family sans
+\emph on
+Descripción
+\family default
+\emph default
+ se añade al final 
+\family sans
+{
+\emph on
+valor1
+\emph default
+, 
+\family default
+...
+\family sans
+}
+\family default
+, estos valores se pueden usar en la semántica.
+\end_layout
+
+\begin_layout Standard
+Entre las operaciones encontramos 
+\series bold
+constructores
+\series default
+, operaciones cuya semántica no se define y que sirven para definir elementos
+ del TAD, y tales que, si es posible, un elemento del TAD debería tener
+ representación única en términos de estos.
+ El resto son de 
+\series bold
+modificación
+\series default
+ o de 
+\series bold
+consulta
+\series default
+ según si devuelven un elemento del conjunto asociado al TAD o de otro tipo,
+ respectivamente.
+\end_layout
+
+\begin_layout Standard
+Si una operación que normalmente devuelve valores de tipo 
+\family sans
+T
+\family default
+ no esta definida para cierta entrada, se crea un conjunto 
+\family sans
+M
+\family default
+ de mensajes cuya descripción contiene al final 
+\family sans
+{
+\begin_inset Quotes fls
+\end_inset
+
+
+\emph on
+Texto mensaje 1
+\emph default
+
+\begin_inset Quotes frs
+\end_inset
+
+, 
+\family default
+...
+\family sans
+}
+\family default
+, y el conjunto resultado de la operación se declara 
+\family sans
+T
+\begin_inset Formula $\cup$
+\end_inset
+
+M
+\family default
+, mientras que en Maude se crea un tipo de errores 
+\family typewriter
+NoT
+\family default
+ con un constructor sin parámetros para cada tipo de error y se usa 
+\family typewriter
+subsort No
+\emph on
+T
+\emph default
+ < 
+\emph on
+T
+\family default
+\emph default
+ para indicar que toda operación que toda operación que devuelva un valor
+ de 
+\family typewriter
+\emph on
+T
+\family default
+\emph default
+ también puede devolver uno de 
+\family typewriter
+No
+\emph on
+T
+\family default
+\emph default
+.
+\end_layout
+
+\begin_layout Standard
+La semántica consiste en una serie de reglas que, dada una expresión, Maude
+ va comprobando de arriba a abajo sucesivamente para ver si parte de la
+ expresión coincide con 
+\family sans
+\emph on
+ExprA
+\family default
+\emph default
+ y sustituirla en tan caso por 
+\family sans
+\emph on
+ExprB
+\family default
+\emph default
+ hasta que no queden sustituciones por hacer, momento en que la expresión
+ debería estar en términos de constructores.
+ Una expresión tiene sintaxis 
+\family typewriter
+\emph on
+op
+\family default
+\emph default
+[
+\family typewriter
+(
+\emph on
+par1
+\emph default
+, 
+\family default
+...
+\family typewriter
+)
+\family default
+], donde los parámetros de la operación son a su vez otras expresiones.
+ 
+\family sans
+\emph on
+ExprB
+\family default
+\emph default
+ o alguna de sus subexpresiones puede ser 
+\family sans
+\series bold
+SI
+\series default
+ 
+\emph on
+condición
+\emph default
+ 
+\begin_inset Formula $\implies$
+\end_inset
+
+ 
+\emph on
+valorSiCierto
+\emph default
+ | 
+\emph on
+valorSiFalso
+\family default
+\emph default
+, o en Maude, 
+\family typewriter
+if 
+\emph on
+condición
+\emph default
+ then 
+\emph on
+valorSiCierto
+\emph default
+ else 
+\emph on
+valorSiFalso
+\emph default
+ fi
+\family default
+.
+\end_layout
+
+\begin_layout Standard
+En Maude, fuera de la definición de un TAD podemos usar 
+\family typewriter
+in 
+\emph on
+nombre
+\emph default
+ .
+
+\family default
+ para leer todo lo que hay en un fichero llamado 
+\family typewriter
+\emph on
+nombre
+\family default
+\emph default
+ o 
+\family typewriter
+\emph on
+nombre
+\emph default
+.maude
+\family default
+ o 
+\family typewriter
+red 
+\emph on
+expr
+\family default
+\emph default
+ para reducir una expresión según la semántica de las operaciones.
+ Un fallo en Maude puede tiene consecuencias impredecibles porque Maude
+ es una mierda.
+\end_layout
+
+\begin_layout Standard
+Si el orden de las reglas no es relevante las llamamos axiomas
+\begin_inset Foot
+status open
+
+\begin_layout Plain Layout
+Cada vez que llamas axiomas a algo que depende del orden muere un matemático
+ y un gatito.
+\end_layout
+
+\end_inset
+
+, y estos deben cumplir las propiedades de 
+\series bold
+completitud
+\series default
+ (deben ser suficientes para deducir el significado de cualquier expresión)
+ y 
+\series bold
+corrección
+\series default
+; dicho de otra forma, se deben considerar todos los casos al definir cada
+ operación no constructora.
+\end_layout
+
+\begin_layout Section
+Órdenes de ejecución
+\end_layout
+
+\begin_layout Standard
+Medimos el tiempo que tarda en ejecutarse un algoritmo con una función 
+\begin_inset Formula $t:\mathbb{N}\rightarrow\mathbb{R}^{\geq0}$
+\end_inset
+
+ para cada uno de los casos mejor, peor y promedio, que toma el tamaño del
+ problema medido de algún modo y devuelve el tiempo que tarda en realizarse
+ en cierta máquina, el número de instrucciones total o el de un tipo de
+ instrucción que sabemos que es la más relevante.
+ En la práctica se usan 
+\series bold
+notaciones asintóticas
+\series default
+:
+\end_layout
+
+\begin_layout Itemize
+\begin_inset Formula $f(x)=O(g(x)):\iff\exists x_{0},k>0:\forall x\geq x_{0},|f(x)|\leq k|g(x)|$
+\end_inset
+
+.
+\end_layout
+
+\begin_layout Itemize
+\begin_inset Formula $f(x)=\Omega(g(x)):\iff\exists x_{0},k>0:\forall x\geq x_{0},kg(x)\leq f(x)$
+\end_inset
+
+.
+\end_layout
+
+\begin_layout Standard
+\begin_inset Note Comment
+status open
+
+\begin_layout Itemize
+\begin_inset Formula $f(x)=\Theta(g(x)):\iff f(x)=O(g(x))\land f(x)=\Omega(g(x))$
+\end_inset
+
+.
+\end_layout
+
+\begin_layout Itemize
+\begin_inset Formula $f(x)=o(g(x)):\iff\lim_{x\rightarrow+\infty}\frac{f(x)}{g(x)}=0$
+\end_inset
+
+.
+\end_layout
+
+\end_inset
+
+
+\end_layout
+
+\begin_layout Standard
+Estas definiciones sólo son válidas cuando 
+\begin_inset Formula $x$
+\end_inset
+
+ tiende a 
+\begin_inset Formula $+\infty$
+\end_inset
+
+.
+\end_layout
+
+\end_body
+\end_document