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.
Example:
-- The operation `head` does not fail if this condition is satisfied:
head'nonfail xs = not (null xs)
head (x:xs) = xNote that the non-failing precondition is not a precondition for
head in the sense of contract-based programming, 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 failedNote that this might be the result translating the following definition:
abs x | x>=0 = x
| x<0 = 0 - xThis requires reasoning on integer arithmetic, as supported by SMT solvers.
Depending on the state of the operation error, this
could also verify the absence 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)If 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.
The current implementation uses the Z3 theorem prover, i.e., the
executable z3 must be in the path when using the
tool.
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