From b530497ca1975ff31b8ecc4f2d6fec00bdced615 Mon Sep 17 00:00:00 2001 From: "Ogilvie, D.H. (Duncan)" <d.h.ogilvie2@students.uu.nl> Date: Thu, 26 Oct 2017 10:47:32 +0200 Subject: [PATCH] readme --- README.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 0cc533e..8b272d9 100644 --- a/README.md +++ b/README.md @@ -77,7 +77,10 @@ Postcondition B will be mapped to: To facilitate further development, it was decided to use an intermediate representation for logical expressions. The frontend converts the Java EDSL to the IR and the backend uses IR to implement the comparison of two expressions. -You can find the source code in `src/LogicIR/Expr.hs` TODO +You can find the source code in `src/LogicIR/Expr.hs` TODO N is numeric + +TODO: future work, sets, types +TODO: parse logicir from file ### LogicIR.Frontend @@ -87,10 +90,13 @@ Currently there is only one frontend for the Java EDSL, but this could quite eas One of the implemented backends is for the [Z3 Theorem Prover](https://github.com/Z3Prover/z3). The `LogicIR.Expr` is converted to a `Z3 AST`. +TODO: valid (invalid), satisfiable (unsatisfiable) +TODO: + To determine if two expressions (`P` and `Q`) are equal, we ask Z3 to prove `P != Q`. There are three possible results: -1. `Sat` -> Z3 proved `P != Q`, which means the two formulas are *not* equivalent. The Z3 model contains the counter example to provide to the student. -2. `Unsat` -> Z3 proved that `P != Q` does not hold, which means the two formulas are equivalent. +1. `Sat` -> Z3 proved `P != Q` is satisfiable, which means the two formulas are *not* equivalent. The Z3 model contains the counter example to provide to the student. +2. `Unsat` -> Z3 proved that `P != Q` is not satisfiable, which means the two formulas are equivalent. 3. `Undef` -> Z3 was unable to decide the satisfiablity of `P != Q`. In this case we have to resort to other methods like QuickCheck to determine if the two formulas are equivalent or not. #### Notes -- GitLab