-- | Encodes a security lattice. module SME.Lattice where -- | Type class to encode security lattices. class Eq a => Lattice a where -- | The greatest lower bound between two security levels. meet :: a -> a -> Maybe a -- | The lowest upper bound between two security levels. join :: a -> a -> Maybe a -- | Type class to encode finite security lattices. class Lattice a => FiniteLattice a where -- | All the elements in the lattice. universe :: [a] -- | It returns all the elements in the lattice that are strictly above the security level given as argument. upset :: a -> [a] -- upper set -- | Implementation of the order relationship between elements of the lattice. less :: Lattice a => a -> a -> Bool less l h = case h `meet` l of Nothing -> False Just r -> h == r -- | Implementation of the strict order relationship between security levels of the lattice. sless :: Lattice a => a -> a -> Bool sless p q = p `less` q && p /= q