Commit 1db23949 authored by Kai Prott's avatar Kai Prott
Browse files


parent c65ac9a0
......@@ -73,3 +73,40 @@ The second one is a standalone tool that can only do the verification.
To use it, just execute `elm-verify` in the directory of an Elm project
or specify a source file to verify. (E.g. `elm-verify src/Main.elm`.)
To enable debug output one can pass `-v` as the first parameter to elm-verify.
How to specify verifiable conditions:
Suppose you have the following code (simplified):
fac : Int -> Int
fac n = if n == 0 then 1 else n * fac (n-1)
Then you can add a the pre and postconditions with this code:
fac_pre_nonNegative : Int -> Bool
fac_pre_nonNegative n = n >= 0
fac_post_positive : Int -> Int -> Bool
fac_post_positive _ n = n >= 1
So the naming scheme is `functionName_pre_conditionName`.
(The name is optional)
One could also use type invariants like this:
type alias Natural = Int
natural_inv : Int -> Bool
natural_inv n = n >= 0
fac : Natural -> Natural
fac n = if n == 0 then 1 else n * fac (n-1)
This automatically adds the invariant as a pre and postcondition to fac.
\ No newline at end of file
Supports Markdown
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