有没有用于防护分析的工具?

rub*_*ect 2 logic haskell

我是一个Haskell noob,在阅读Haskell Road中的Implications时,我开始关注拼图.

verdict :: Bool -> Bool -> (Bool, String)
verdict p q | not result  = (False, "LIAR")
            | result && p = (True,  "telling the truth")
            | result      = (True,  "innocent unless proven guilty")
            | otherwise   = (False, "we shouldn't get here")
  where result = (not p) || q
-- map (\x -> verdict (fst x == 1) (snd x == 1)) [(1,1),(1,0),(0,1),(0,0)]
Run Code Online (Sandbox Code Playgroud)

是否有工具可以警告我其他类似或其他类似的逻辑错误?

Dan*_*ner 8

我想我会以不同的方式编写这个函数:

-- not result
verdict True  False = (False, "LIAR")
-- result && p
verdict True  True  = (True , "telling the truth")
-- result
verdict False _     = (True , "innocent unless proven guilty")
verdict _     True  = (True , "innocent unless proven guilty")
-- otherwise
verdict _     _     = (False, "we shouldn't get here")
Run Code Online (Sandbox Code Playgroud)

那么不仅人类可以忽略哪些条款(最后两个),而且机器也是如此; ghc在默认警告级别说:

test.hs:2:5: Warning:
    Pattern match(es) are overlapped
    In an equation for ‘verdict’:
        verdict _ True = ...
        verdict _ _ = ...
Run Code Online (Sandbox Code Playgroud)

一般检查警卫重叠当然是不可判定的; 此外,我不知道会尝试给出一个近似答案的工具.