Commit 22a083cb authored by Michael Hanus 's avatar Michael Hanus
Browse files

README updated, non-determinism example added

parent 239dc141
......@@ -5,14 +5,13 @@ 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
the correct arguments which satisfy the non-failing precondition of
the operation.
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 precondition is satisfied:
head_nonfail xs = not (null xs)
head'nonfail xs = not (null xs)
head (x:xs) = x
......@@ -28,7 +27,9 @@ is non-failing:
if null ws then readCommand
else processCommand (head ws) (tail ws)
The following techniques to verify non-failing properties are used:
A detailed description can be found in the
[PPDP 2018 paper](https://doi.org/10.1145/3236950.3236957).
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)
......@@ -39,18 +40,18 @@ The following techniques to verify non-failing properties are used:
are used with satisfied non-failing preconditions
for all inputs satisfying the non-failing precondition.
3. Test whether a call to `Prelude.fail` is unreachable, e.g., in
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 fail
else failed
Note that this might be the result translating the following definition:
abs x | x>=0 = x
| x<0 = 0 - x
This requires SMT solving...
This requires reasoning on integer arithmetic, as supported by SMT solvers.
Depending on the state of the operation `error`,
......@@ -63,7 +64,8 @@ this could also avoid the occurrence of run-time errors:
else do putStr "First char: "
putStrLn (head s)
If `error` is considered as an always failing operation,
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`)
......@@ -74,7 +76,7 @@ which might raise exceptions.
Current restrictions:
---------------------
- The nonfail specification should be a Boolean formula, i.e.,
- 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.
......@@ -85,16 +87,16 @@ Current restrictions:
Notes:
------
- Contracts and nonfail specifications can also be stored in separate
- 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, the contents of `m_SPEC` is added to `m` before
it is checked.
- nonfail specifications for operators can be also specified by
operations named by `op_xh1...hn'`, where
each `hi` is a two digit hexadecimal number, into the name
of corresponding to the ord values of `h1...hn`.
For instance, the nonfail specification for `&>` can be named
- 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`.
- Operations defining contracts and properties are not verified.
......
-- Non-deterministic list insertion.
-- Both rules are overlapping. Thus, if the Curry evaluator
-- decides to take the second rule, the evaluation fails on the
-- empty list.
ins :: a -> [a] -> [a]
ins x ys = x : ys
ins x (y:ys) = y : ins x ys
-- Therefore, the following non-fail condition is required:
ins'nonfail :: a -> [a] -> Bool
ins'nonfail _ _ = False
-- To provide a non-failing version of list insertion, we define
-- a non-deterministic list insertion by pattern matching:
insP :: a -> [a] -> [a]
insP x [] = [x]
insP x (y:ys) = x : y : ys ? y : insP x ys
-- Exploiting non-deterministic list insertion, one can easily define
-- list permutations:
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = insP x (perm xs)
......@@ -2,7 +2,7 @@
--- A tool to verify non-failure properties of Curry operations.
---
--- @author Michael Hanus
--- @version April 2018
--- @version August 2018
---------------------------------------------------------------------------
module Main where
......@@ -39,6 +39,8 @@ import ToolOptions
import TypedFlatCurryGoodies
import VerifierState
------------------------------------------------------------------------
-- To support testing:
test :: Int -> String -> IO ()
test v = verifyNonFailingMod defaultOptions { optVerb = v }
......@@ -51,7 +53,7 @@ testv = test 3
banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "Fail-Free Verification Tool for Curry (Version of 27/04/18)"
bannerText = "Fail-Free Verification Tool for Curry (Version of 30/08/18)"
bannerLine = take (length bannerText) (repeat '=')
---------------------------------------------------------------------------
......
......@@ -2,7 +2,7 @@
--- The options of the non-failing analysis tool.
---
--- @author Michael Hanus
--- @version April 2018
--- @version August 2018
-------------------------------------------------------------------------
module ToolOptions
......@@ -78,7 +78,7 @@ options =
"check contracts w.r.t. strict evaluation strategy"
, Option "t" ["time"]
(NoArg (\opts -> opts { optTime = True }))
"check contracts w.r.t. strict evaluation strategy"
"show total verification time for each module"
]
where
safeReadNat opttrans s opts =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment