ManTa
Fundamentación
Rodrigo Cardoso
Universidad de los Andes
Depto. de Ing. de Sistemas y Computación
Contenido
1 TADs ecuacionales
2 Semántica
3 Variantes de definición
4 Prueba de teoremas sobre TADs
5 Implantación abstracta
6 Implantación concreta
ManTa: Fundamentación
2
1 TADs ecuacionales
•
Un Tipo Abstracto de Datos ( TAD ) es una estructura algebraica
heterogénea
•
TAD =  Signatura , Axiomas 
•
La signatura es una declaración de operaciones o funciones y sus
funcionalidades
•
Los axiomas son predicados que condicionan las operaciones del
TAD.
•
En un TAD ecuacional, todos los axiomas son ecuaciones.
ManTa: Fundamentación
3
TAD Cola [ X ]

Cola

Cola
Cola

bool
:
Cola

X
:
Cola

Cola
*
vac
:
*
ins
:
Cola
esvac
:
prim
ati
x
X
Axiomas
[ev1]
[ev2]
esvac ( vac )
esvac ( ins ( c, x ) )
= true
= false
[pr1]
[pr2]
prim ( vac )
prim ( ins ( c, x ) )
= 
= if
esvac ( c )
then x
else prim ( c )
fi
[at1]
[at2]
ati ( vac )
ati ( ins ( c, x ) )
= vac
= if
esvac ( c )
then vac
else ins( ati ( c ), x )
fi
DAT
ManTa: Fundamentación
4
Notación para TADs
TDI
Tipos primitivos
TAD Y [ X1, X2, …, Xn ]
…
* gj : Aj
…
…
sk : Ak
x
Yp j
ManTa: Fundamentación
Y
generadoras
selectoras
x
Ypk
…
Axiomas
…
s k ( a k , y1 ) = …
s k ( a k , y2 ) = …
…
DAT


Z
A i = X i1 x X i2 x … x X ir
pi  0
Z  { X1, X2, …, Xn, Y }
5
Clasificación de operaciones
Típicamente:
f:
Xi1 x Xi2 x … x Xi2 x Ym

Z
Iniciales
( m = 0, Z = Y )
[ vac ]
Constructoras
( m > 0, Z = Y )
[ ins ]
Simplificadoras
( m  0, Z = Y )
[ ati ]
Analizadoras
( m > 0, Z = Xik )
[ prim ]
Generadoras
Funciones
Selectoras
ManTa: Fundamentación
6
El lenguaje del TAD
• La signatura determina el lenguaje del TAD.
• Se definen términos y axiomas.
• Los términos sirven para denotar objetos.
Cada término tiene un tipo asociado.
• Hay TADs parámetros dados (v.gr., nat, bool, …)
• Los axiomas establecen relaciones de igualdad entre términos del
mismo tipo, i.e., entre denotaciones de objetos.
ManTa: Fundamentación
7
Términos
•
Un término atómico es una constante primitiva, una variable o indefinido.
•
Una constante primitiva es un elemento de un TAD parámetro.
El tipo de una constante es el TAD al que pertenece.
•
Las variables son tomadas de un conjunto enumerable.
El tipo de una variable depende del contexto en que aparezca.
•
El término indefinido (  ) representa valores de error.
El tipo {  } se considera incluido en todo TAD.
•
Un término compuesto ( de tipo Z ) tiene la forma
donde
f ( t1,…, tr )
f : A1 x … x Ar  Z
ti
ManTa: Fundamentación
es un símbolo de función
es término de tipo Ai
8
Términos (cont.)
•
Un término condicional ( de tipo Z ) tiene la forma
if  término de tipo bool  then  término de tipo Z 
else  término de tipo Z 
fi
•
Un término ( de tipo Z ) es uno atómico, compuesto o condicional, de tipo Z.
•
Cualquier término que hace parte de otro es un subtérmino.
•
Un término es básico si no contiene variables ni subtérminos indefinidos.
ManTa: Fundamentación
9
Axiomas
•
Los axiomas tienen la forma
LI
=
LD
donde:
– L I es un término compuesto f ( t1,…, tr ) que no contiene
subtérminos condicionales.
– L D es un término
– Los tipos de L I y L D coinciden
•
Las variables:
– tienen alcance local a los axiomas
– se consideran cuantificadas universalmente
– su tipo es determinable unívocamente del contexto en que
aparecen
ManTa: Fundamentación
10
El tipo de interés ( TDI )
Se define el TDI:
Y

términos atómicos generados por G y variables,
más el elemento  (indefinido)
v.gr.
Cola =
{  , vac,
ins ( vac, x1 ), ins ( vac, x2 ),
..., ins ( ins ( vac, x1 ), x1 ), ...
}
ManTa: Fundamentación
11
Reducción de términos
•
Los axiomas pueden utilizarse para reescribir términos
•
Se usan de izquierda a derecha
•
Definen una relación de reducibilidad ( .  . )
•
Por ejemplo:
ins ( ati ( vac ), x )  ins ( vac, x )
ya que
ati ( vac ) = vac
Notación:
•
e1

e2
ssi
Hay un axioma aplicable a e1 y el resultado es e2
•
e1
 e2
ssi
e1 = u1  ...  ur = e2
•
e1

e2
ssi
e1  e2
•
e1

e2
ssi
e1 = u1  ...  ur = e2
( r - equivalencia )
ManTa: Fundamentación
ó
(r0)
e2  e1
(r0)
12
Semántica de un TAD Y
•
Un término representa un objeto (real o ya entendido)
•
e1  e2
:
“e2 es más simple que e1”
“valen ( significan ) lo mismo”
•
e1  e2
•
Se deberían preferir las expresiones simples ( reducidas )
•
Así: para averiguar el valor de un término, se busca reducirlo a otro
equivalente
:
“e1 y e2 significan lo mismo”
más simple
ojalá ya entendido
ManTa: Fundamentación
13
Significado de los términos
•
e
es irreducible si no se puede reescribir
Por ejemplo:
vac,
•
e
x,
ins ( vac, x )
es una forma normal de e’ si
e es irreducible
e’ e
Elegir una forma normal como significado ( o valor ) de e
e puede no tener formas normales
e puede tener varias formas normales
e puede tener formas normales que se desearía reducir ( ! )
ManTa: Fundamentación
14
Cuándo es “buena” la definición de un TAD ?
Dos criterios:
•
Sintáctico
:
completitud suficiente
Conseguible por construcción, siguiendo una
metodología
•
Semántico
:
distinguibilidad de objetos
Dependiente de las intenciones del diseñador
ManTa: Fundamentación
15
Completitud suficiente
•
Y [ X1, …, Xn ] es suficientemente completo si todo término e
de tipo Xi reduce a un elemento x de Xi , i.e.,
e x
•
Por ejemplo:
e
=
prim ( ins ( ati ( vac ), x ) )

if
esv ( vac )
then
x
else
prim ( vac )
x
else
fi

if

x
ManTa: Fundamentación
true
then
…
fi
16
Para qué un TAD suficientemente completo ?
•
e x , x  Xi
x es una forma normal para e
•
En un TAD suficientemente completo:
Todo término de tipo primitivo evalúa a un objeto primitivo , i.e.,
Todo término de tipo primitivo tiene significado conocido
•
Ejemplo:
Si en TAD Cola [ X ] se omitiera el axioma
ati ( vac ) = vac
e =
prim ( ins ( ati ( vac ), x ) )

if esv ( ati ( vac ) )
then x
else
prim ( ati ( vac ) )
fi
que es irreducible.
No habría significado “natural”.
ManTa: Fundamentación
17
Distinguibilidad
•
Si dos objetos son distinguibles, sus nombres deben ser diferenciables
•
Objetos distinguibles

Hay una característica que
los diferencia
•
Nombres diferenciables

Hay una selectora que
los diferencia
•
Si ninguna selectora diferencia los nombres de dos objetos diferentes,
faltan selectoras
•
En caso contrario, se dirá que el TAD es discriminante.
ManTa: Fundamentación
18
Qué pasa si no hay distinguibilidad ?
Se sabe que:
a

a
b
Los nombres correspondientes son:
e1 = ins ( vac , a )
e2 = ins ( ins ( vac , a ), b )
Nótese que:
esv ( e1 ) = esv ( e2 )
prim ( e1 ) = prim ( e2 )
Pero:
ati ( e1 ) = ins ( vac , b )
ati ( e2 ) = vac
Y puesto que:
esv ( ins ( vac, b ) ) = false  true = esv ( vac )
También:
e1  e2
ManTa: Fundamentación
19
Igualdad definida
•
Deseable: definir una operación de igualdad
eq-Y : Y  Y  bool
•
eq-Y es una congruencia para el álgebra de términos del TAD, i.e., es
compatible con la reescritura.
•
Variante: definición implícita mediante funciones caracterizadoras.
•
ManTa permite definición implícita de igualdades, pero no comprueba
que lo sean.
ManTa: Fundamentación
20
Interpretación del TAD Y
•
Todo término básico debe tener exactamente una forma normal.
•
Un término básico se interpreta como su forma normal.
•
La reescritura es el mecanismo de cálculo de significado de los
términos.
•
Los axiomas deben definir comportamientos funcionales para las
operaciones.
– Más que completitud suficiente, el comportamiento funcional
conlleva completitud.
– ManTa ayuda a verificar la unicidad de los significados, pero no la
terminación del proceso de reescritura.
No hay medidas de complejidad de los términos.
•
El modelo definido es el modelo inicial de la estructura algebraica.
ManTa: Fundamentación
21
3 Variantes de definición
•
Instanciación
TAD W [ X1 ]  Y [ X1 , X2 ] DAT
•
Producto cartesiano
TAD W [ X1, X2 ]  Y1 [ X1 ]  Y2 [ X2 ] DAT
•
Sumas
TAD W [ X1, X2 ]  Y1 [ X1 ]  Y2 [ X2 ] DAT
•
Restricción
TAD W [ X ]  ( Y [ X ] : restr )
restr : Y  bool
...
DAT
ManTa: Fundamentación
22
Semántica de las variantes de definición
•
Siempre expresable en términos de la semántica estándar.
•
Detalles adicionales en algunas de ellas
v.gr., en productos cartesianos, definición de proyecciones.
•
Los TADs definidos por variantes deben heredar características de
aquellos en los que su definición se apoya.
•
ManTa no sobrecarga operadores ( no maneja herencia en el sentido
de POO ).
•
Falta poder definir TADs que dependen de parámetros que no son
TADs, sino objetos, v.gr.,
TAD Intervalo ( m , n ) = m .. n DAT
TAD Zn DAT
ManTa: Fundamentación
23
4 Prueba de teoremas sobre TADs
•
ManTa sólo prueba teoremas expresables como ecuaciones.
•
Para probar un teorema M = N se procede así:
[ 1 ] Normalizar
Reducir M y N a sus formas normales M* y N*.
Si M*  N* , responder afirmativamente.
[ 2 ] Inducción estructural
Sobre las variables del TDI, usar esquemas de inducción.
Si hay éxito, responder afirmativamente.
Si no, intentar generalización.
[ 3 ] Prueba semántica
Si eq-Y( M* , N*) * true , responder afirmativamente.
En otro caso, responder “no se sabe”.
ManTa: Fundamentación
24
Más sobre la prueba de teoremas ...
•
Las pruebas siguen un esquema similar al del probador de Boyer &
Moore.
•
Es adecuado ( eficiente ) el orden del procedimiento de prueba ?
•
ManTa no aprovecha lemas ya demostrados para otras pruebas.
•
Cómo manejar los lemas no orientables ?
ManTa: Fundamentación
25
5 Implantación abstracta
•
Una implementación (  , P )
de TAD Y ( fuente ) en TAD W ( objeto ) consta de:
[a]  : W  Y
( representación )
función recursiva, parcial, sobre
[ b ] Para cada Y-función f , un W-programa p que la interpreta.
P es el conjunto de estos programas
•
Esquemáticamente, se tienen situaciones como:
f
Y
Y
Y



p
W
ManTa: Fundamentación
W
f
X
p
W
26
Representación 
•
La función de representación
 :
•
W  Y
 es definida recursivamente sobre la construcción de Y ( LFN ! ).
Así se garantiza que sea sobre.
•
O sea:
 se explica haciendo corresponder a cada Y-generadora un Wprograma que calcula su representación
v.gr.,
empty
=
 ( vac )
push (  ( c ) , x ) =
 ( ins ( c , x ) )
•
Una implementación queda descrita al indicar qué W-programa
interpreta cada Y-función
ManTa: Fundamentación
27
ImpTAD
[SCem]
[SCpu]
Stack [ X ]  Cola [ X ] : 
empty
push (  ( c ) , x )
=  ( vac )
=  ( ins ( c , x ) )
[SCpo]
[SCto]
[SCie]
[SCsz]
pop (  ( c ) )
top (  ( c ) )
isempty (  ( c ) )
size (  ( c ) )
=  ( ant ( c ) )
= ult ( c )
= esv ( c )
= tam ( c )
[SCeq]
eq-stack (  ( c1 ) ,  ( c2 ) )
Operaciones auxiliares
ant :
Cola

Cola
ult :
Cola

X
Axiomas auxiliares
[an1]
[an2]
[ul1]
[ul2]
ant ( vac )
ant ( ins ( c , x ) )
ult ( vac )
ult ( ins ( c , x ) )
=
=
=
=
= eq-cola ( c1, c2 )
vac
c

x
DATpmI
ManTa: Fundamentación
28
Composición de implantaciones
Supónganse dos implantaciones (  , P ), (  , Q )
Y

W : 
W

Z : 
Entonces:

Y
Z
:
°
es una implantación ( ° , P ° Q ) , donde
•
° ( z )
=  ( (z))
•
P ° Q
= { fWZ | f Y-función, fWZ interp. fW en Z }
°
Y

W

ManTa: Fundamentación
Z
29
Verificación de implementación
•
Los axiomas del TAD fuente deben ser verificados por la representación
•
Por ejemplo:
isempty ( empty )
=
isempty (  ( vac ) )
, por [ SCem ]
=
esv ( vac )
, por [ SCie ]
=
true
, por [ ev1 ]
=
isempty ( push (  ( c ) , x )
, porque  es sobre
=
isempty (  ( ins ( c , x ) ) )
, por [ SCpu ]
=
esv ( ins ( c , x ) )
, por [ SCie ]
=
false
, por [ ev2 ]
isempty ( push ( s, x ) )
ManTa: Fundamentación
30
Verificar

Demostrar teoremas
•
Caso general: verificar un axioma corresponde a demostrar un
teorema en el TAD que representa
•
Los teoremas son siempre ecuaciones
•
Como  es sobre, las variables del TAD fuente se pueden
remplazar por  -imágenes de variables del TAD objeto, v.gr., F
( c ) en lugar de s.
•
Métodos de demostración de teoremas:
Sintácticos
Reducción a términos equivalentes
Inducción sobre la construcción
Semánticos
Chequeo de igualdad
ManTa: Fundamentación
31
Reducción a términos equivalentes
Para demostrar
e1 = e2
se usan:
Programas definidos en la implementación
Axiomas del TAD que representa
como reglas de reescritura
v.gr.:
isempty ( empty )
ManTa: Fundamentación
=
isempty (  ( vac ) )
, por [ SCem ]
=
esv ( vac )
, por [ SCie ]
=
true
, por [ ev1 ]
32
6 Implementación concreta
•
La composición de implementaciones es una implementación
•
El último TAD puede ser una estructura computacional EC , i.e.,
objetos y operaciones que manipula un lenguaje de programación
Y
W1
W2
...
Wn
EC
ManTa: Fundamentación
33
El paso a lo concreto
•
El paso
Y  EC
se dificulta, porque usualmente no se cuenta con una descripción
axiomática de la EC.
•
La definición de la implementación varía según el lenguaje de
programación que manipule EC, v.gr.,
un lenguaje funcional ( Lisp, Scheme, CAML , ... )
un lenguaje imperativo ( Pascal , C , ... )
etc.
ManTa: Fundamentación
34
Implementación en un lenguaje funcional
•
No es difícil:
Si los axiomas del TAD describen funciones recursivas, éstas son
casi directamente programables en el lenguaje funcional objeto
•
Es fácil construir prototipos funcionales para TADs
( y con ellos, constatar experimentalmente la adecuación a la
realidad, la corrección, etc. )
ManTa: Fundamentación
35
Ejemplo:
Cola [ nat ]  Lisp : 
vac
ins (  [ lista ] , n )
esv (  [ lista ] )
prim (  [ lista ] )
=
=
=
=
 [ nil ]
 [ ( cons n lista ) ]
( null lista )
( priml lista )
donde:
( priml lista )

( cond
( ( null lista )
( ( null ( cdr lista ) )
(t
“indefinido” )
( car lista ) )
( priml (cdr lista ) ) )
)
La definición de priml se deriva “naturalmente” de los axiomas de prim
ManTa: Fundamentación
36
Implementación en un lenguaje imperativo
•
Un lenguaje imperativo es usualmente eficiente
•
Preferible usar procedimientos que cambian argumentos que
pasan por referencia
•
Método:
Representar elementos del TDI mediante estructuras de datos
del lenguaje de programación
v.gr., arreglos , apuntadores a estructuras dinámicas, etc.
Para cada función, derivar de los axiomas una pre- y una
poscondición
Programar cumpliendo la especificación
ManTa: Fundamentación
37
Implementación automática en ManTa
•
ManTa ha funcionado con prototipos funcionales ( Lisp ) e imperativos (
C ).
•
ManTa 3.0 genera prototipos C y un “banco de pruebas” para
experimentar con la implantación concreta.
•
Parece fácil generar prototipos CAML.
•
Línea de acción: desarrollo de herramientas y métodos de
transformación de programas que mantengan la semántica y mejoren
la eficiencia.
ManTa: Fundamentación
38
Descargar

ppt - ManTa