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:

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., inabs 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.

- The non-fail condition should be a Boolean formula, i.e., not a function with pattern matching or local definitions. Furthermore, it should be a first-order equation, i.e., in eta-expanded form.

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