Tema 16: El tipo abstracto de datos de las colas de prioridad

• inserta x (inserta y c) == inserta y (inserta x c)
• primero (inserta x vacia) == x
• Si x <= y, entonces primero (inserta y (inserta x c)) == primero (inserta x c)
• resto (inserta x vacia) == vacia
• Si x <= y, entonces resto (inserta y (inserta x c)) == inserta y (resto (inserta x c))
• esVacia vacia
• not (esVacia (inserta x c))

• Cabecera del módulo:

  module Tema_16.ColaDePrioridadConListas
    (CPrioridad,
     vacia,   -- Ord a => CPrioridad a
     inserta, -- Ord a => a -> CPrioridad a -> CPrioridad a
     primero, -- Ord a => CPrioridad a -> a
     resto,   -- Ord a => CPrioridad a -> CPrioridad a
     esVacia, -- Ord a => CPrioridad a -> Bool
     valida   -- Ord a => CPrioridad a -> Bool
    ) where
  

• Colas de prioridad mediante listas:

  newtype CPrioridad a = CP [a]
    deriving (Eq, Show)
  

• Ejemplo: La cola de prioridad obtenida añadiéndole a la cola vacía los elementos 3, 1, 7, 2 y 9 es

  λ> foldr inserta vacia [3,1,7,2,9]
  CP [1,2,3,7,9]
  

• (valida c) se verifica si c es una cola de prioridad válida; es decir, está ordenada crecientemente. Por ejemplo,

  valida (CP [1,3,5])  ==  True
  valida (CP [1,5,3])  ==  False
  

  Su definición es

  valida :: Ord a => CPrioridad a -> Bool
  valida (CP xs) = ordenada xs
    where ordenada (x:y:zs) = x <= y && ordenada (y:zs)
          ordenada _        = True
  

• vacia es la cola de prioridad vacía. Por ejemplo,

  λ> vacia
  CP []
  

  Su definición es

  vacia :: Ord a => CPrioridad a
  vacia = CP []
  

• (inserta x c) es la cola obtenida añadiendo el elemento x a la cola de prioridad c. Por ejemplo,

  λ> inserta 5 (foldr inserta vacia [3,1,7,2,9])
  CP [1,2,3,5,7,9]
  

  Su definición es

  inserta :: Ord a => a -> CPrioridad a -> CPrioridad a
  inserta x (CP q) = CP (ins x q)
    where ins x []                   = [x]
          ins x r@(e:r') | x < e     = x:r
                         | otherwise = e:ins x r'
  

• (primero c) es el primer elemento de la cola de prioridad c.

  primero (foldr inserta vacia [3,1,7,2,9])  ==  1
  

  Su definición es

  primero :: Ord a => CPrioridad a -> a
  primero (CP(x:_)) = x
  primero _         = error "primero: cola vacia"
  

• (resto c) es la cola de prioridad obtenida eliminando el primer elemento de la cola de prioridad c. Por ejemplo,

  resto (foldr inserta vacia [3,1,7,2,9])  ==  CP [2,3,7,9]
  

  Su definición es

  resto :: Ord a => CPrioridad a -> CPrioridad a
  resto (CP (_:xs)) = CP xs
  resto _           = error "resto: cola vacia"
  

• (esVacia c) se verifica si la cola de prioridad c es vacía. Por ejemplo,

  esVacia (foldr inserta vacia [3,1,7,2,9]) ==  False
  esVacia vacia  ==  True
  

  Su definición es

  esVacia :: Ord a => CPrioridad a -> Bool
  esVacia (CP xs) = null xs
  

La implementación de las colas de prioridad como montículos (ColaDePrioridadConMonticulos.hs) se encuentra en el tema 20 (El TAD de los montículos).

• Al principio del fichero se añade

  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  

• Importación de la implementación de colas de prioridad que se desea verificar.

  import Tema-16.ColaDePrioridadConListas
  -- import Tema_20.ColaDePrioridadConMonticulos
  -- import I1M.ColaDePrioridad
  

• Importación de las librerías de comprobación

  import Test.QuickCheck
  

• genCPrioridad es un generador de colas de prioridad. Por ejemplo,

  λ> sample genCPrioridad
  CP [-4]
  CP [-2,-1,-1,2,5]
  ...
  

  genCPrioridad :: (Arbitrary a, Num a, Ord a) =>  Gen (CPrioridad a)
  genCPrioridad = do
    xs <- listOf arbitrary
    return (foldr inserta vacia xs)
  
  instance (Arbitrary a, Num a, Ord a) => Arbitrary (CPrioridad a) where
    arbitrary = genCPrioridad
  

• Las colas de prioridad producidas por genCPrioridad son válidas.

  prop_genCPrioridad_correcto ::  CPrioridad Int -> Bool
  prop_genCPrioridad_correcto c = valida c
  

• Comprobación.

  λ> quickCheck prop_genCPrioridad_correcto
  +++ OK, passed 100 tests.
  

• Si se añade dos elementos a una cola de prioridad se obtiene la misma cola de prioridad idependientemente del orden en que se añadan los elementos.

  prop_inserta_conmuta :: Int -> Int -> CPrioridad Int -> Bool
  prop_inserta_conmuta x y c =
    inserta x (inserta y c) == inserta y (inserta x c)
  

• La cabeza de la cola de prioridad obtenida anadiendo un elemento x a la cola de prioridad vacía es x.

  prop_primero_inserta_vacia :: Int -> CPrioridad Int -> Bool
  prop_primero_inserta_vacia x c =
    primero (inserta x vacia) == x
  

• El primer elemento de una cola de prioridad c no cambia cuando se le añade un elemento mayor o igual que algún elemento de c.

  prop_primero_inserta :: Int -> Int -> CPrioridad Int -> Property
  prop_primero_inserta x y c =
    x <= y ==>
    primero (inserta y c') == primero c'
    where c' = inserta x c
  

• El resto de añadir un elemento a la cola de prioridad vacía es la cola vacía.

  prop_resto_inserta_vacia :: Int -> Bool
  prop_resto_inserta_vacia x =
    resto (inserta x vacia) == vacia
  

• El resto de la cola de prioridad obtenida añadiendo un elemento y a una cola c' (que tiene algún elemento menor o igual que y) es la cola que se obtiene añadiendo y al resto de c'.

  prop_resto_inserta :: Int -> Int -> CPrioridad Int -> Property
  prop_resto_inserta x y c =
    x <= y ==>
    resto (inserta y c') == inserta y (resto c')
    where c' = inserta x c
  

• vacia es una cola vacía.

  prop_vacia_es_vacia :: Bool
  prop_vacia_es_vacia = esVacia (vacia :: CPrioridad Int)
  

• Si se añade un elemento a una cola de prioridad se obtiene una cola no vacía.

  prop_inserta_no_es_vacia :: Int -> CPrioridad Int -> Bool
  prop_inserta_no_es_vacia x c =
    not (esVacia (inserta x c))
  

• Para verificar todas las propiedades se escribe

  return []
  verifica = $quickCheckAll
  

• Comprobación de las propiedades de las colas de prioridad

  λ> verifica
  === prop_genCPrioridad_correcto from ColaDePrioridadPropiedades.hs:45 ===
  +++ OK, passed 100 tests.
  
  === prop_inserta_conmuta from ColaDePrioridadPropiedades.hs:59 ===
  +++ OK, passed 100 tests.
  
  === prop_primero_inserta_vacia from ColaDePrioridadPropiedades.hs:69 ===
  +++ OK, passed 100 tests.
  
  === prop_primero_inserta from ColaDePrioridadPropiedades.hs:79 ===
  +++ OK, passed 100 tests.
  
  === prop_resto_inserta_vacia from ColaDePrioridadPropiedades.hs:90 ===
  +++ OK, passed 100 tests.
  
  === prop_resto_inserta from ColaDePrioridadPropiedades.hs:101 ===
  +++ OK, passed 100 tests.
  
  === prop_vacia_es_vacia from ColaDePrioridadPropiedades.hs:111 ===
  +++ OK, passed 1 tests.
  
  === prop_inserta_no_es_vacia from ColaDePrioridadPropiedades.hs:120 ===
  +++ OK, passed 100 tests.
  
  True