5. Diccionario de Prejos Binarios
5.0 Tipo Abstracto de Dato
TAD Diccionario de Prefijos Binarios ()
parametros formales
generos
extiende dicc(secu(nat), )
usa nat, secu(nat)
exporta genero, generadores, observadores basicos, prejoValido
generos diccPB()
generadores
denir : secu(nat) s    diccPB() 􀀀! diccPB()(prejoValido(s))
observadores basicos
def? : secu(nat)  diccPB() 􀀀! bool
obtener : secu(nat) s  diccPB() d 􀀀!  (def?(s, d))
otras operaciones
prejoValido : secu(nat) 􀀀! bool
esPrejo : secu(nat)  secu(nat) 􀀀! bool
axiomas 8s; s0 : secu(nat), 8a : , 8d : diccPB(), 8e : nat
def?(s, vaco)  false
def?(s, denir(s', a, d)  esPrejo(s', s) _ def?(s, d)
obtener(s, denir(s', a, d))  if esPrejo(s', s) then a else obtener(s, d)
prejoValido(s)  vaca?(s) _L (prim(s)  1 ^ prejoValido(n(s)))
esPrejo(<>, s)  true
esPrejo(e  s', s)  : (vaca?(s)) ^L (e = prim(s) ^ esPrejo(s', n(s))
Fin TAD