The objective is this tool is to verify that all operations are non-failing, i.e., their evaluation does not result in a failure, if they are called with arguments satisfying the non-failing precondition of the operation.
-- The operation `head` does not fail if this precondition is satisfied: head'nonfail xs = not (null xs) head (x:xs) = x
Note that the non-failing precondition is not a precondition for
head, i.e., it is still allowed to use
head in a logical setting. However, it can be used to verify that the following operation is non-failing:
readCommand = do putStr "Input a command:" s <- getLine let ws = words s if null ws then readCommand else processCommand (head ws) (tail ws)
A detailed description can be found in the PPDP 2018 paper. Basically, the following techniques are used to verify non-failing properties:
Test whether the operation is pattern-completely defined (i.e., branches on all patterns in all or-branches) for all inputs satisfying the non-failing precondition. If this is not the case, the operation is possibly failing.
Test whether the operations called in the right-hand side are used with satisfied non-failing preconditions for all inputs satisfying the non-failing precondition.
Test whether a call to
Prelude.failed is unreachable, e.g., in
abs x = if x>=0 then x else if x<0 then (0 - x) else failed
Note that this might be the result translating the following definition:
abs x | x>=0 = x | x<0 = 0 - x
This requires reasoning on integer arithmetic, as supported by SMT solvers.
Depending on the state of the operation
error, this could also avoid the occurrence of run-time errors:
readLine = do putStr "Input a non-empty string:" s <- getLine if null s then error "Empty input!" else do putStr "First char: " putStrLn (head s)
error is considered as an always failing operation (which is done if the option
--error is set),
readLine cannot be verified as non-failing. However, this requires also a careful analysis of all external operations (like
readFile) which might raise exceptions.
Contracts and non-fail conditions can also be stored in separate files. When checking a module
m, if there is a Curry module
m_SPEC in the load path for module
m or in the package directory
include, the contents of
m_SPEC is added to
m before it is checked.
Non-fail conditions for operators can also be specified by operations named by
op_xh1...hn', where each
hi is a two digit hexadecimal number and the name of the operator corresponds to the ord values of
h1...hn. For instance, the non-fail condition for
&> can be named
op_x263E'nonfail. To generate such names automatically, one can use the option
--name of the tool.
Operations defining contracts and properties are not verified.
examples: some examples (and test suite)
include: an include file for the SMT solver and non-fail conditions for various system modules
src: source code of the implementation