|
dependencies:
|
[Dependency "base" [[VGte "3.2.0",VLt "4.0.0"]],Dependency "abstract-curry" [[VGte "4.0.0",VLt "5.0.0"]],Dependency "cass" [[VGte "4.0.0",VLt "5.0.0"]],Dependency "cass-analysis" [[VGte "4.0.0",VLt "5.0.0"]],Dependency "containers" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "contracts" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "csv" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "currypath" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "directory" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "execpath" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "extra" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "filepath" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "flatcurry" [[VGte "3.0.0",VLt "5.0.0"]],Dependency "flatcurry-smt" [[VMajCompatible "2.0.0"]],Dependency "io-extra" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "json" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "process" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "profiling" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "rw-data" [[VGte "1.0.0"]],Dependency "scc" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "time" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "transformers" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "wl-pprint" [[VGte "3.0.0",VLt "4.0.0"]],Dependency "xml" [[VGte "3.0.0",VLt "4.0.0"]]]
|
|
documentation:
|
A tool to verify Curry operations as non-failing
================================================
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 xs
In 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) = x
and
tail (x:xs) = xs
have 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](http://dx.doi.org/10.1007/978-981-97-2300-3\_10),
Arithmetic non-fail conditions
------------------------------
If the SMT solver [Z3](https://github.com/Z3Prover/z3.git) 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)
The ideas of the verification of arithmetic non-fail conditions
are described in:
> M. Hanus: Hybrid Verification of Declarative Programs with
> Arithmetic Non-fail Conditions,
> Proc. of the 22nd Asian Symposium on Programming Languages and Systems
> (APLAS 2024), Springer LNCS 15194, pp. 109-129, 2024,
> DOI: [10.1007/978-981-97-8943-6\_6](http://dx.doi.org/10.1007/978-981-97-8943-6\_6),
------------------------------------------------------------------------------
Installation
------------
If you downloaded the sources of this package, then the tool can be
installed via the command
> cypm install
in the main directory of this package. Otherwise, the tool can
also be downloaded and installed by the command
> cypm install verify-non-fail
This 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.
------------------------------------------------------------------------------
Web Demo Installation
---------------------
If you want to try this tool on simple programs via a web interface,
you can use a
[Web Demo Installation](https://cpm.curry-lang.org/webapps/failfree/)
of this tool.
------------------------------------------------------------------------------
Files
-----
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-CALLTYPES
provided 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
------------------------------------------------------------------------------
|