diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -2,6 +2,10 @@ ## Unreleased changes +- Polish documentation +- Update tests for FPTaylor v0.9.4 + - v0.9.4 is much faster in some cases and produces slightly different (often slightly better) bounds. + ## [v0.1.1.0](https://github.com/rasheedja/PropaFP/compare/v0.1.0.0...v0.1.1.0) - Remove quotes from FPTaylor variables, allowing support for FPTaylor >=0.9.3 diff --git a/PropaFP.cabal b/PropaFP.cabal --- a/PropaFP.cabal +++ b/PropaFP.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4. +-- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack name: PropaFP -version: 0.1.1.0 +version: 0.1.2.0 synopsis: Auto-active verification of floating-point programs description: Please see the README on GitHub at category: Math, Maths, Mathematics, Formal methods, Theorem Provers diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -4,20 +4,20 @@ PropaFP can be used for the verification of [SPARK][1]/[Ada][2] floating-point programs and is integrated with [GNAT Studio 2022](https://www.adacore.com/gnatpro/toolsuite/gnatstudio). PropaFP can take some Verification Condition (VC), and if PropaFP understands the VC, simplify it, derive bounds for variables, and safely eliminate floating-point operations using over-approximations on rounding errors. -A more detailed description of PropaFP can be found in [this paper](https://arxiv.org/abs/2207.00921). +A more detailed description of PropaFP can be found in [this paper](https://link.springer.com/chapter/10.1007/978-3-031-17108-6_2) ([arXiv version](https://arxiv.org/abs/2207.00921)). Below is a diagram summarising the integration with PropaFP and SPARK. -![SPARK + PropaFP](https://github.com/rasheedja/PropaFP/raw/v0.1.1.0/images/SPARK_Toolchain_PropaFP.png) +![SPARK + PropaFP](images/SPARK_Toolchain_PropaFP.png) [1]: https://en.wikipedia.org/wiki/SPARK_(programming_language) [2]: https://en.wikipedia.org/wiki/Ada_(programming_language) ## Requirements -All PropaFP executables require the [FPTaylor v0.9.3](https://github.com/soarlab/FPTaylor/releases/tag/v0.9.3) executable in your $PATH. +All PropaFP executables require the [FPTaylor v0.9.4](https://github.com/soarlab/FPTaylor/tree/efbbc83970fe3c9f4cb33fafbbe1050dd18749cd) executable in $PATH. -The 'propafp-run-$prover' executables require you to have $prover installed (but not necessarily in your $PATH). +The 'propafp-run-$prover' executables require the $prover to be installed (but not necessarily in $PATH). To build PropaFP, we recommend [Stack](https://docs.haskellstack.org/en/stable/README/). We have built PropaFP with Stack version 2.7.5. @@ -27,7 +27,7 @@ - cd into the repo - Run `stack build` -Stack will then build the project and tell you where the PropaFP executables have been placed. +Stack will then build the project and state where the PropaFP executables have been placed. ### Supported Provers @@ -43,7 +43,7 @@ ### PropaFP as a Standalone Program -To produce some input for PropaFP, see the [Reference](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/REFERENCE.md). +To produce some input for PropaFP, see the [Reference](REFERENCE.md). #### Translator Executables @@ -59,19 +59,19 @@ #### Runner Executables 'Runner' executables take some input file, transform the VC as described above, and calls the prover on the transformed VC. -'Runner' executables require the prover for each executable to be in your $PATH. +'Runner' executables require the prover for each executable to be in $PATH. The current 'runner' executables are: - propafp-run-dreal -f [smtFileContainingVC.smt2] -p [pathToDReal] - propafp-run-lppaver -f [smtFileContainingVC.smt2] -p [pathToLPPaver] - propafp-run-metitarski -f [smtFileContainingVC.smt2] -p [pathToMetiTarski] -To run LPPaver in a mode specialised to find counter-examples, you can pass the -c option. +To run LPPaver in a mode specialised to find counter-examples, pass the -c option. ### PropaFP with GNAT Studio -For instructions to use with GNAT Studio 2022, see [sparkFiles/INSTRUCTIONS.md](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/sparkFiles/INSTRUCTIONS.md) +For instructions to use with GNAT Studio 2022, see [sparkFiles/INSTRUCTIONS.md](sparkFiles/INSTRUCTIONS.md) ## Guided Example -[A guided example of using PropaFP with GNAT Studio.](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/sparkFiles/EXAMPLE.md) +[A guided example of using PropaFP with GNAT Studio.](sparkFiles/EXAMPLE.md) diff --git a/src/PropaFP/Parsers/Smt.hs b/src/PropaFP/Parsers/Smt.hs --- a/src/PropaFP/Parsers/Smt.hs +++ b/src/PropaFP/Parsers/Smt.hs @@ -792,7 +792,7 @@ (Just ff1, Just ff2) -> Just $ FConn Or ff1 ff2 (_, _) -> Nothing filterOutVars (FConn Impl f1 f2) vars False = - case (filterOutVars f1 vars False, filterOutVars f2 vars False) of + case (filterOutVars f1 vars True, filterOutVars f2 vars False) of (Just ff1, Just ff2) -> Just $ FConn Impl ff1 ff2 (_, _) -> Nothing filterOutVars (FConn And f1 f2) vars True = @@ -806,9 +806,9 @@ (_, Just ff2) -> Just ff2 (_, _) -> Nothing filterOutVars (FConn Impl f1 f2) vars True = - case (filterOutVars f1 vars True, filterOutVars f2 vars True) of + case (filterOutVars f1 vars False, filterOutVars f2 vars True) of (Just ff1, Just ff2) -> Just $ FConn Impl ff1 ff2 - (Just ff1, _) -> Just ff1 + (Just ff1, _) -> Just $ FNot ff1 (_, Just ff2) -> Just ff2 (_, _) -> Nothing filterOutVars (FNot f) vars isNegated = FNot <$> filterOutVars f vars (not isNegated)