packages feed

PropaFP 0.1.1.0 → 0.1.2.0

raw patch · 4 files changed

+19/−15 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

ChangeLog.md view
@@ -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
PropaFP.cabal view
@@ -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 <https://github.com/rasheedja/PropaFP#readme> category:       Math, Maths, Mathematics, Formal methods, Theorem Provers
README.md view
@@ -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)
src/PropaFP/Parsers/Smt.hs view
@@ -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)