start creating a new experiment, based on Wermer's original.

README.md

-### To run the mutation test:
+# javawlp Library
 
-- Create the mutation files using Major in the right location (described below):
-	$MAJOR_HOME/bin/javac -J-Dmajor.export.directory="$SOURCE mutants" -J-Dmajor.export.mutants=true -XMutator:ALL -cp "wlp/tests" wlp/Tests/$SOURCE.java
-- Edit settings.hs to specify the post-condition and test file
-- Run the main function (this can be done using ghci)
-- The results will be stored in wlp/Results, overwriting any existing results file that uses the same parameters (the analysis is static, so the results should be the same in this case anyway)
+javawlp is a Haskell library that implements Dijkstra's weakest pre-condition transformer that targets the Java programming language. 
+Given a statement *stmt* and a post-condition *q*, the transformer *wlp stmt q* calculates the weakest pre-condition for the statement
+to establish the post-condition q. Originally, the transformer is used in the context of a programming logic:
+to prove that a Hoare triple specification *{p} stmt {q}* is valid we can instead prove that the
+implication *p implies (wlp stmt q)* is valid. Over the years, predicate transformers are also used for other purposes,
+such as to aid software testing.
 
-### To run the false positive test:
+The weakest pre-condition of loops and recursions is unfortunately in general uncomputable. javawlp takes the pragmatic approach
+to unroll loops and recursions some finite number of times (configurable). As such, verification through javawlp falls
+in the category bounded verification.
 
-- Edit settings.hs to specify the post-condition
-- Run the testFalsePositives function (this can be done using ghci)
-- The results will be stored in wlp/Results
+Copyright (c) 2017, Utrecht University
 
-### Folder structure:
+Authors: Koen Wermer, Wishnu Prasetya
 
-The folder generated by Major must be in the same folder as the wlp folder, and must be named "SOURCE mutants" (where SOURCE is the name of the test class)
-A path to a mutant (the 5th mutant in this example) looks like this: "SOURCE mutants/5/classPath/SOURCE.java" Because of this, to analyse a new test class the classPath function in Settings.hs has to be extended with the corresponding class path
+License: GPL
+
+### How to deploy
+
+TO DO: Provide a cabal file.
+
+javawlp is distributed as a Haskell library. The main functions exported by the library can be found in the module `Javawlp.API`.
+
+Example of use:
+
+```
+module Mymodule where
+import Javawlp.API
+test = do -- parse a Java source file; specify the path to the file:
+          (tyenv,decls,methods) <- parseJava filepath  
+          configuration <- defaultConf
+          -- specify a post-condition and calculate the wlp:
+          p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
+          -- do something with the obtained wlp (p):
+          putStrLn (prettyPrint p)
+```
+
+You can check the obtained pre-condition for its satisfiability and obtained the value assignment that
+satisfies it as shown below. This is for example useful to obtain a test case. 
+
+```
+module Mymodule where
+import Javawlp.API
+import Z3.Monad
+import Javawlp.Engine.Verifier
+import Javawlp.Engine.HelperFunctions
+test = do -- this part is as in the previous example:
+          (tyenv,decls,methods) <- parseJava filepath  
+          configuration <- defaultConf
+          p <- wlpMethod configuration tyenv decls (Ident methodname) (post_ "returnValue == 0")
+          -- now check p's satisfiability and print its model: 
+          let (result,model) = unsafeIsSatisfiable (extendEnv tyenv decls (Ident methodname)) decls p
+          case result of
+             Sat   -> do 
+                      let (Just m) = model
+                      s <- evalZ3 (modelToString m)
+                      putStrLn ("SATISFIABLE. Model: " ++ s)
+             Unsat -> putStrLn "Not satisfiable."
+             _     -> putStrLn "Unable to decide."  
+```
+
+### Content
+
+- src: contains javawlp's source files.
+- papers: includes Wermer's original thesis. 
+- examples: includes a set of small Java examples you can try as targets for the wlp transformer.
 
 ### Dependency
 
-- language-java Haskell package
\ No newline at end of file
+Haskell packages:
+
+- language-java 
+- z3 (this is not the actual z3, but provides interface to z3)
+
+Other software:
+
+- You will need the actual z3
\ No newline at end of file