FOP/ex2.1 - 大久保弘崇

2.1

prop_InsertOrdered x = forAll orderedList $ \ xs ->
  let xxs = x:xs
      ins = insert x xs
  in  ordered ins && sameContents xxs ins
 
sameContents xs ys = null (xs \\ ys) && null (ys \\ xs)
 

2.2

マージ

merge xxs@(x:xs) yys@(y:ys) | x <= y = x:merge xs yys
                            | True   = y:merge xxs ys
merge xs [] = xs
merge [] ys = ys
 
prop_MergeOrdered :: Property
prop_MergeOrdered = forAll orderedList body where
  body :: [Integer] -> Property
  body xs =
    forAll orderedList $ \ ys ->
      let mgs = merge xs ys
          aps = xs ++ ys
      in  ordered mgs && sameContents mgs aps
 

マージソート

msort :: Ord a => [a] -> [a]
msort [] = []
msort [x] = [x]
msort xs = merge (msort us) (msort vs) where
  (us, vs) = splitAt (length xs `div` 2) xs
 
prop_Msort :: [Integer] -> Bool
prop_Msort xs = ordered (msort xs)
 

2.3

-- 実行可能仕様
type Buffer = (Int, String)
empty = (0, "") :: Buffer
insert :: Char -> Buffer -> Buffer
insert c (p, s) = (p+1, take p s ++ c : drop p s)
delete :: Buffer -> Buffer
delete (p, s) = (p-1, take (p-1) s ++ drop p s)
left (p, s) = (p-1, s)                   ; left :: Buffer -> Buffer
right (p, s) = (p+1, s)                  ; right :: Buffer -> Buffer
atLeft (p, _) = p == 0                   ; atLeft :: Buffer -> Bool
atRight (p, s) = p == length s           ; atRight :: Buffer -> Bool
 
-- 効率的実装
type BufferI = (String, String)
emptyI = ("", "") :: BufferI
insertI c (a, b) = (c:a, b)              ; insertI :: Char -> BufferI -> BufferI
deleteI (c:a, b) = (a, b)                ; deleteI :: BufferI -> BufferI
leftI (c:a, b) = (a, c:b)                ; leftI :: BufferI -> BufferI
rightI (a, c:b) = (c:a, b)               ; rightI :: BufferI -> BufferI
atLeftI (a, _) = null a                  ; atLeftI :: BufferI -> Bool
atRightI (_, b) = null b                 ; atRightI :: BufferI -> Bool
 
-- 回収関数
retreiveI :: BufferI -> Buffer
retreiveI (a, b) = (length a, foldl (flip (:)) b a) -- reverse' a b
 
-- テスト
prop_empty = retreiveI emptyI == empty
prop_insert c a b = (retreiveI $ insertI c (a,b)) == (insert c $ retreiveI (a,b))
prop_delete (NonEmpty a) b = (retreiveI $deleteI (a,b))==(delete$ retreiveI (a,b))
prop_left (NonEmpty a) b = (retreiveI $ leftI (a,b)) == (left $ retreiveI (a,b))
prop_right a (NonEmpty b) = (retreiveI $ rightI (a,b))==(right $ retreiveI (a,b))
prop_atleft  a b = atLeftI  (a,b) == (atLeft  $ retreiveI (a,b))
prop_atright a b = atRightI (a,b) == (atRight $ retreiveI (a,b))
 

2.4

代数的仕様と標準形は秘匿する。

prop_i c c' buf = insertI c (leftI (insertI c' buf)) == leftI (insertI c' (insertI c buf))
prop_d1 c buf = not (atLeftI buf) ==> deleteI (leftI (insertI c buf)) == leftI (insertI c (deleteI buf))
prop_d2 c buf = deleteI (insertI c buf) == buf
prop_r buf = not (atLeftI buf) ==> rightI (leftI buf) == buf
prop_al1 = atLeftI emptyI == True
prop_al2 c buf = atLeftI (insertI c buf) == False
prop_al3 c buf = atLeftI (leftI (insertI c buf)) == atLeftI buf
prop_ar1 = atRightI emptyI == True
prop_ar2 c buf = atRightI (insertI c buf) == atRightI buf
prop_ar3 buf = not (atLeftI buf) ==> atRightI (leftI buf) == False
-- prop_l buf buf' c c' = not (atLeftI buf) && leftI buf == leftI (insertI c' buf') ==> leftI (leftI (insertI c buf)) == leftI (insertI c' (leftI (insertI c buf')))
prop_l buf' c c' = not (atLeftI buf) && leftI buf == leftI (insertI c' buf') ==> leftI (leftI (insertI c buf)) == leftI (insertI c' (leftI (insertI c buf'))) where buf = insertI c' buf'
 

prop_lはコメントの物が代数的仕様に対応するが、quickCheck的な都合で変形した。

コメント