failfree: A tool for verifying fail-free Curry programs

Basic idea of the tool:

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) = x

Note 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:

  1. 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.

  2. 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.

  3. 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 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.


Current restrictions:


Notes:


Directories of the package: