This package contains a tool to verify that all operations in a given Curry module are non-failing, i.e., their evaluation does not result in a failure, if they are called with appropriate arguments. The tool automatically infers abstract call types and non-fail conditions specifying supersets of appropriate arguments.
As an example, consider the following operation to compute the last element of a given list:
last :: [a] -> a
last [x] = x
last (_ : xs@(_:_)) = last xsIn the default mode (where types are abstracted into a set of allowed top-level constructors), the inferred call type is
last: {:}specifying that last does not fail if the argument is a
non-empty list, i.e., evaluable to some data term rooted by the list
constructor “:”.
When an operation with such a restricted call type is used, the tool checks whether it is used in a context which ensures its call type. For instance, the operations
head (x:xs) = xand
tail (x:xs) = xshave the inferred call types
head: {:}
tail: {:}When these operations are applied, it should be ensured (in a top-level functional computation) that the actual arguments are non-empty lists, as in the following operation:
readCommand :: IO ()
readCommand = do
putStr "Input a command:"
s <- getLine
let ws = words s
case null ws of True -> readCommand
False -> processCommand (head ws) (tail ws)The tool automatically verifies that the operation
readCommand is non-failing.
The ideas of the implementation of this tool are described in:
M. Hanus: Inferring Non-Failure Conditions for Declarative Programs, Proc. of the 17th International Symposium on Functional and Logic Programming (FLOPS 2024), Springer LNCS 14659, pp. 167-187, 2024, DOI: 10.1007/978-981-97-2300-3_10,
If the SMT solver Z3
is installed and the executable z3 can be found in the
path, the tool can also infer and verify arithmetic non-fail conditions.
For instance, it infers for the factorial function defined by
fac :: Int -> Int
fac n | n == 0 = 1
| n > 0 = n * fac (n - 1)the non-fail condition
fac'nonfail :: Int -> Bool
fac'nonfail v1 = (v1 == 0) || (v1 > 0)specifying that the argument must be non-negative in order to ensure
that fac does not fail. With this information, it also
proves that the following I/O operation does not fail (where the
operation readInt reads a line until it is an integer):
printFac :: IO ()
printFac = do
putStr "Factorial computation for: "
n <- readInt
if n<0 then putStrLn "Negative number, try again" >> printFac
else print (fac n)If you downloaded the sources of this package, then the tool can be installed via the command
> cypm installin the main directory of this package. Otherwise, the tool can also be downloaded and installed by the command
> cypm install verify-non-failThis installs the executable curry-calltypes in the
bin-directory of CPM.
If one uses KiCS2 to install this tool, one should use version 3.1.0 of April 11, 2024 (or newer) due to a memory leak in an older version of KiCS2.
If you want to try this tool on simple programs via a web interface, you can use a Web Demo Installation of this tool.
In order to support a modular analysis of applications consisting of
several modules, the tool caches already computed analysis results of
modules in under the directory ~/.curry_verify_cache. This
path is defined in Verify.Files.getVerifyCacheDirectory. To
store the analysis results for different Curry systems and abstract
domains separately, the analysis results for a Curry module which is
stored in a file with path MODULEPATH.curry are contained
in
~/.curry_verify_cache/CURRYSYSTEMID/DOMAINID/MODULEPATH-*For instance, the call types of the prelude for KiCS2 Version 3.1.0
w.r.t. the abstract domain Values are stored in
~/.curry_verify_cache/kics2-3.1.0/Values/opt/kics2/lib/Prelude-CALLTYPESprovided that KiCS2 is installed at /opt/kics2 so that
the prelude is contained in the file
/opt/kics2/lib/Prelude.curry.
All cache files (for the Curry system used to install this tool) can be deleted by the command
curry-calltypes --delete