README.md

# javawlp Library

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.

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.

Copyright (c) 2017, Utrecht University

Authors: Koen Wermer, Wishnu Prasetya

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

Haskell packages:

- language-java 
- z3 (this is not the actual z3, but provides interface to z3)

Other software:

- You will need the actual z3

### Pre-processing 

Some limitations in the current implementation requires the target source code to meet certain 
syntactical constraints; so some pre-processing is required before a source file can be exposed
to javawlp.

- Reference to an instance member x should be explicitly written as this.x
- Binary subexpressions should be explicitly parathesized since our parser does not take
  Java's built in operators priority into account. So, instead of `x==y && x+z>0` write
  `(x==y) && ((x+z)>0)`