SSVT Exam 2018

exam.hs

module Exam2018 where

import           Data.Char
import           Data.List
import           Test.QuickCheck


-- Hoare Triples --

-- Use this to validate a Hoare triple respectively to find a counter-example (Domain: Integers)
check_HoareTester :: Testable prop => (Integer -> Bool) -> (Integer -> Integer) -> (Integer -> prop) -> IO ()
check_HoareTester preCond func postCond = verboseCheck (withMaxSuccess testAmount hoareTester)
  where
    testAmount  = 1000
    hoareTester = constructHoareTester preCond func postCond

constructHoareTester :: Testable prop => (Integer -> Bool) -> (Integer -> Integer) -> (Integer -> prop) -> (Integer -> Property)
constructHoareTester preCond func postCond = (\ x -> preCond x ==> postCondTester x func postCond)

postCondTester :: a -> (a -> b) -> (b -> c) -> c
postCondTester input func postCond = postCond . func $ input

manualHoareTester :: Integer -> Integer -> Property
manualHoareTester x n = (x < (0)) && (n > 0) ==> postCondTester x (\x -> x^2 + x) (\ x -> x > 0)



-- Relations --

type Rel a = [(a,a)]

arbitrary_RelInteger = do
    rs <- generate arbitrary :: IO (Rel Integer)
    let ds = sort . nub . concat $ (map (\ r -> fst r : snd r : []) rs)
    return (ds, rs)


-- Relation validity checks


-- Reflexive

isReflexive :: Eq a => [a] -> Rel a -> Bool
isReflexive ds rs = all (==True) [(d, d) `elem` rs | d <- ds]

-- prop_AtLeastCardinalityOfDomainMembers =


-- Irreflexive

isIrreflexive :: Eq a => [a] -> Rel a -> Bool
isIrreflexive ds rs = any (==True) [not((d, d) `elem` rs) | d <- ds]


-- Transitive

isTransitive :: Eq a => Rel a -> Bool
isTransitive rs = all (==True) (concat [map (\ cr -> (r1, snd cr) `elem` rs) (filter (\ r -> fst r == r2) rs) | (r1, r2) <- rs])

-- If a relation is transitive, its inverse relation should be transitive as well.
prop_InverseIsTransitive :: Property
prop_InverseIsTransitive =
  forAll (choose (1 :: Int, 10 :: Int)) $ \ n ->
    let rs = transitiveRelationOnDomain [0..n] in
    isTransitive . inverseRelation $ rs


-- Symmetric

isSymmetric :: Eq a => Rel a -> Bool
isSymmetric rs = all (==True) [(r2, r1) `elem` rs | (r1, r2) <- rs]

-- If a relation is symmetric, its inverse relation should be symmetric as well.
prop_InverseIsSymmetric :: Property
prop_InverseIsSymmetric =
  forAll (choose (1 :: Int, 50 :: Int)) $ \ n ->
    let rs = symmetricRelationOnDomain [0..n] in
    isSymmetric . inverseRelation $ rs


-- Asymmetric

isAsymmetric :: Eq a => Rel a -> Bool
isAsymmetric rs = all (==True) [not((r2, r1) `elem` rs) && (r1 /= r2) | (r1, r2) <- rs]

-- If a relation is antisymmetric, its inverse relation should be antisymmetric as well.
prop_InverseIsAsymmetric :: Rel Int -> Property
prop_InverseIsAsymmetric rs = isAsymmetric rs ==> isAsymmetric . inverseRelation $ rs


-- Antisymmetric

isAntisymmetric :: Eq a => Rel a -> Bool
isAntisymmetric rs = all (==True) [not((r2, r1) `elem` rs) || r1 == r2 | (r1, r2) <- rs]

-- If a relation is antisymmetric, its inverse relation should be antisymmetric as well.
prop_InverseIsAntisymmetric :: Rel Int -> Property
prop_InverseIsAntisymmetric rs = isAntisymmetric rs ==> isAntisymmetric . inverseRelation $ rs


-- Equivalence Relation

isEquivalenceRelation :: Eq a => [a] -> Rel a -> Bool
isEquivalenceRelation ds rs = (isReflexive ds rs) && (isTransitive rs) && (isSymmetric rs)


-- Linear

isLinear :: Eq a => [a] -> Rel a -> Bool
isLinear ds rs = all (==True) [((d1, d2) `elem` rs) || ((d2, d1) `elem` rs) | d1 <- ds, d2 <- ds, d1 /= d2]

-- prop_LinearRelationCardinalityRequirement =
--   forAll (choose (1 :: Int, 50 :: Int)) $ \ n ->
--     let rs = symmetricRelationOnDomain [0..n] in
--     isSymmetric . inverseRelation $ rs



-- Relation generators

inverseRelation :: Rel a -> Rel a
inverseRelation rs = [(r2, r1) | (r1, r2) <- rs]

reflexiveClosure :: Ord a => Rel a -> Rel a
reflexiveClosure rs = sort . nub $ (rs ++ dupReflexive)
  where
    dupReflexive = concat [[(r1, r1)] ++ [(r2, r2)] | (r1, r2) <- rs]

transitiveClosure :: Ord a => Rel a -> Rel a
transitiveClosure rs = sort . nub $ (rs ++ dupTransitive)
  where
    dupTransitive = concat [map (\ r -> (r1, snd r)) (filter (\ r -> fst r == r2) rs) | (r1, r2) <- rs]

symmetricClosure :: Ord a => Rel a -> Rel a
symmetricClosure rs = sort . nub $ (rs ++ dupSymmetric)
  where
    dupSymmetric = [(r2, r1) | (r1, r2) <- rs]

reflexiveTransitiveClosure :: Ord a => Rel a -> Rel a
reflexiveTransitiveClosure = transitiveClosure . reflexiveClosure

equivalenceClosure :: Ord a => Rel a -> Rel a
equivalenceClosure = symmetricClosure . reflexiveTransitiveClosure

linearClosure :: Ord a => Rel a -> Rel a
linearClosure rs = linearClosureOnDomain domain
  where
    domain = nub . concat $ [r1 : r2 : [] | (r1, r2) <- rs]

linearClosureOnDomain :: Ord a => [a] -> Rel a
linearClosureOnDomain ds = map (\ ral -> (ral !! 0, ral !! 1)) relsAsLists
  where
    relsAsLists = nub (map sort [[d1, d2] | d1 <- ds, d2 <- ds, d1 /= d2])

partitions :: [a] -> [[[a]]]
partitions []     = [[]]
partitions (d:ds) = [p | pps <- partitions ds, p <- prependPerms d pps]
  where
    prependPerms :: a -> [[a]] -> [[[a]]]
    prependPerms d []       = [[[d]]]
    prependPerms d (ds:dss) = ((d:ds):dss) : map (ds:) (prependPerms d dss)

-- START -- Test properties: partitions
-- 1) If one unions each of the partitions, the original domain (set) will form.
prop_UnionPartitionsToGetOriginalSet :: [Int] -> Property
prop_UnionPartitionsToGetOriginalSet ds = length ds <= 8 ==> all (\ u -> sort u == sort ds) [concat p | p <- partitions ds]

check_UnionPartitionsToGetOriginalSet = verboseCheck prop_UnionPartitionsToGetOriginalSet
-- END -- Test properties: partitions

reflexiveRelationOnDomain :: Ord a => [a] -> Rel a
reflexiveRelationOnDomain ds = [(d, d) | d <- ds]

symmetricRelationOnDomain :: Ord a => [a] -> Rel a
symmetricRelationOnDomain ds = sort . nub . concat $ dupSymmetric
  where
    dupSymmetric = [filter (\ (r1, r2) -> r1 /= r2) (map (\ m -> (d, m)) ds) | d <- ds]

transitiveRelationOnDomain :: Ord a => [a] -> Rel a
transitiveRelationOnDomain ds = sort . nub $ (reflexiveRelationOnDomain ds ++ symmetricRelationOnDomain ds)

equivalenceRelationOnDomain :: Ord a => [a] -> Rel a
equivalenceRelationOnDomain = reflexiveTransitiveClosure . symmetricRelationOnDomain

allEquivalenceRelationsOnDomain :: Ord a => [a] -> [Rel a]
allEquivalenceRelationsOnDomain ds = filter (\ rs -> isEquivalenceRelation ds rs) thinnedPerms
  where
    equivRel      = equivalenceRelationOnDomain ds
    permsEquivRel = permutations equivRel
    thinnedPerms  = nub (map sort (allEquivalenceRelationsOnDomainHelper permsEquivRel (length equivRel)))

allEquivalenceRelationsOnDomainHelper :: [Rel a] -> Int -> [Rel a]
allEquivalenceRelationsOnDomainHelper _ 0  = []
allEquivalenceRelationsOnDomainHelper ps n = (map (\ p -> take n p) ps) ++ allEquivalenceRelationsOnDomainHelper ps (n-1)

-- START -- Test properties: allEquivalenceRelationsOnDomain
prop_amountEquivalenceRelationEqualsAmountPartitions :: Ord a => [a] -> Bool
prop_amountEquivalenceRelationEqualsAmountPartitions ds = amountEquivRel == amountPartitions
  where
    amountEquivRel   = length . allEquivalenceRelationsOnDomain $ ds
    amountPartitions = length . partitions $ ds
-- END -- Test properties: allEquivalenceRelationsOnDomain

cartesianProduct :: [a] -> [a] -> Rel a
cartesianProduct ds1 ds2 = [(d1, d2) | d1 <- ds1, d2 <- ds2]

powerset :: [a] -> [[a]]
powerset []     = [[]]
powerset (d:ds) = (map (d:) (powerset ds)) ++ powerset ds

allPossibleRelations :: [a] -> [Rel a]
allPossibleRelations ds = powerset (cartesianProduct ds ds)

-- START -- Test properties: allPossibleRelations
prop_CardinalityOfAllPossibleRelations :: [Int] -> Property
prop_CardinalityOfAllPossibleRelations ds = length ds <= 4 ==> (length . allPossibleRelations $ ds) == (2^((length ds)^2))

check_CardinalityOfAllPossibleRelations = verboseCheck prop_CardinalityOfAllPossibleRelations
-- END -- Test properties: allPossibleRelations



-- Relation composition

composeRelations :: Ord a => Rel a -> Rel a -> Rel a
composeRelations rs1 rs2 = sort . concat $ composedRels
  where
    composedRels = [map (\ r -> (r1, snd r)) (filter (\ r -> fst r == r2) rs2) | (r1, r2) <- rs1]

composeRelationToPower :: Ord a => Rel a -> Int -> Rel a
composeRelationToPower rs n = composeRelationToPowerHelper rs rs n

composeRelationToPowerHelper :: Ord a => Rel a -> Rel a -> Int -> Rel a
composeRelationToPowerHelper rsO rsC n | n < 2     = rsO
                                       | n == 2    = composeRelations rsO rsC
                                       | otherwise = composeRelationToPowerHelper rsO (composeRelations rsO rsC) (n-1)