Started with expression statements and integrating Z3. Made a simple example run.

Folds.hs

+-- Folds over Java data structures
+module Folds where
+
+import Language.Java.Syntax
+
+type StmtAlgebra r = (Block -> r,           
+                      Exp -> r -> r,        
+                      Exp -> r -> r -> r,
+                      Exp -> r -> r,
+                      (Maybe ForInit) -> (Maybe Exp) -> (Maybe [Exp]) -> r -> r,
+                      [Modifier] -> Type -> Ident -> Exp -> r -> r,
+                      r, 
+                      Exp -> r,
+                      Exp -> (Maybe Exp) -> r,
+                      Exp -> [SwitchBlock] -> r,
+                      r -> Exp -> r,
+                      Maybe Ident -> r,
+                      Maybe Ident -> r,
+                      Maybe Exp -> r, 
+                      Exp -> Block -> r,
+                      Exp -> r,
+                      Block -> [Catch] -> (Maybe Block) -> r,
+                      Ident -> r -> r
+                      )
+                      
+type ExpAlgebra r  = (Literal -> r,           
+                      Maybe Type -> r,        
+                      r,
+                      Name -> r,
+                      [TypeArgument] -> ClassType -> [Argument] -> (Maybe ClassBody) -> r,
+                      r -> [TypeArgument] -> Ident -> [Argument] -> (Maybe ClassBody) -> r,
+                      Type -> [r] -> Int -> r, 
+                      Type -> Int -> ArrayInit -> r,
+                      FieldAccess -> r,
+                      MethodInvocation -> r,
+                      ArrayIndex -> r,
+                      Name -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      r -> r,
+                      Type -> r -> r, 
+                      r -> Op -> r -> r,
+                      r -> RefType -> r,
+                      r -> r -> r -> r,
+                      Lhs -> AssignOp -> r -> r,
+                      LambdaParams -> LambdaExpression -> r,
+                      Ident -> Ident -> r
+                      )
+                      
+
+-- | A fold function over a java statement.
+foldStmt :: StmtAlgebra r -> Stmt -> r
+foldStmt (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) s = fold s where
+    fold s = case s of
+                  StmtBlock b -> fStmtBlock b
+                  IfThen e stmt -> fIfThen e (fold stmt)	
+                  IfThenElse e stmt1 stmt2 -> fIfThenElse e (fold stmt1) (fold stmt2)
+                  While e stmt -> fWhile e (fold stmt)
+                  BasicFor init e incr stmt -> fBasicFor init e incr (fold stmt)
+                  EnhancedFor mods t i e stmt -> fEnhancedFor mods t i e (fold stmt)
+                  Empty -> fEmpty
+                  ExpStmt e -> fExpStmt e
+                  Assert e me -> fAssert e me
+                  Switch e bs -> fSwitch e bs
+                  Do stmt e -> fDo (fold stmt) e
+                  Break l -> fBreak l
+                  Continue l -> fContinue l
+                  Return me -> fReturn me
+                  Synchronized e b -> fSynchronized e b
+                  Throw e -> fThrow e
+                  Try b cs f -> fTry b cs f
+                  Labeled l stmt -> fLabeled l (fold stmt)
+                  
+-- | A fold function over a java expression.
+foldExp :: ExpAlgebra r -> Exp -> r
+foldExp (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) e = fold e where
+    fold e = case e of
+                  Lit lit -> fLit lit
+                  ClassLit mt -> fClassLit mt
+                  This -> fThis
+                  ThisClass name -> fThisClass name
+                  InstanceCreation typeArgs classType args mBody -> fInstanceCreation typeArgs classType args mBody
+                  QualInstanceCreation e typeArgs ident args mBody -> fQualInstanceCreation (fold e) typeArgs ident args mBody
+                  ArrayCreate t exps dim -> fArrayCreate t (map fold exps) dim
+                  ArrayCreateInit t dim arrayInit -> fArrayCreateInit t dim arrayInit
+                  FieldAccess fieldAccess -> fFieldAccess fieldAccess
+                  MethodInv invocation -> fMethodInv invocation
+                  ArrayAccess i -> fArrayAccess i
+                  ExpName name -> fExpName name
+                  PostIncrement e -> fPostIncrement (fold e)
+                  PostDecrement  e -> fPostDecrement  (fold e)
+                  PreIncrement e -> fPreIncrement (fold e)
+                  PreDecrement  e -> fPreDecrement  (fold e)
+                  PrePlus e -> fPrePlus (fold e)
+                  PreMinus e -> fPreMinus (fold e)
+                  PreBitCompl e -> fPreBitCompl (fold e)
+                  PreNot e -> fPreNot (fold e)
+                  Cast t e -> fCast t (fold e)
+                  BinOp e1 op e2 -> fBinOp (fold e1) op (fold e2)
+                  InstanceOf e refType -> fInstanceOf (fold e) refType
+                  Cond g e1 e2 -> fCond (fold g) (fold e1) (fold e2)
+                  Assign lhs assOp e -> fAssign lhs assOp (fold e)
+                  Lambda lParams lExp -> fLambda lParams lExp
+                  MethodRef className methodName -> fMethodRef className methodName
\ No newline at end of file

Main.hs

+module Main where
+
+import Language.Java.Syntax
+import Language.Java.Lexer
+import Language.Java.Parser
+
+import WLP
+
+
+
+
+
+import Language.Java.Pretty
+
+
+main :: IO ()
+main = do
+    source <- readFile "A:\\Thesis\\Test1.java"
+    
+    
+    let result = parser compilationUnit source
+    
+    
+    case result of
+        Left error -> print error
+        Right compUnit -> putStrLn . prettyPrint $ wlp (getStmt compUnit) postCond
+    
+
+-- Gets the statement(-block) defining the main method for simple tests
+getStmt :: CompilationUnit -> Stmt
+getStmt (CompilationUnit _ _ [ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))]) = getInit decls where
+    getInit [] = error "No main method"
+    getInit [MemberDecl (MethodDecl _ _ _ (Ident "main") _ _ (MethodBody (Just b)))] = StmtBlock b
+    getInit (_:decls) = getInit decls
+
+
+-- The post-condition (for testing)
+postCond :: Exp
+postCond = BinOp (ExpName (Name [Ident "x"])) Equal (Lit (Int 1))
\ No newline at end of file

Substitute.hs

+module Substitute where
+
+import Language.Java.Syntax
+
+import Folds
+ 
+
+substVarExpAlgebra :: ExpAlgebra ((Lhs, Exp) -> Exp)
+substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
+    fLit lit _ = Lit lit
+    fClassLit mt _ = ClassLit mt
+    fThis _ = This
+    fThisClass name _ = ThisClass name
+    fInstanceCreation typeArgs classType args mBody _ = InstanceCreation typeArgs classType args mBody
+    fQualInstanceCreation e typeArgs ident args mBody inh = QualInstanceCreation (e inh) typeArgs ident args mBody
+    fArrayCreate t exps dim inh = ArrayCreate t (map ($ inh) exps) dim
+    fArrayCreateInit t dim arrayInit _ = ArrayCreateInit t dim arrayInit
+    fFieldAccess fieldAccess (lhs, rhs) = case lhs of
+                                            FieldLhs fieldAccess' -> case fieldAccess of
+                                                                        PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution"
+                                                                        SuperFieldAccess ident -> error "todo: fieldAccess substitution"
+                                                                        ClassFieldAccess name ident -> error "todo: fieldAccess substitution"
+    fMethodInv invocation _ = MethodInv invocation
+    fArrayAccess (ArrayIndex a is) (lhs, rhs) = case lhs of
+                                                    ArrayLhs arrayIndex -> error "todo: array substitution"
+    fExpName name (lhs, rhs) = case lhs of
+                                    NameLhs name' -> if name == name' then rhs else ExpName name
+    fPostIncrement e inh = PostIncrement (e inh)
+    fPostDecrement e inh = PostDecrement  (e inh)
+    fPreIncrement e inh = PreIncrement (e inh)
+    fPreDecrement e inh = PreDecrement  (e inh)
+    fPrePlus e inh = PrePlus (e inh)
+    fPreMinus e inh = PreMinus (e inh)
+    fPreBitCompl e inh = PreBitCompl (e inh)
+    fPreNot e inh = PreNot (e inh)
+    fCast t e inh = Cast t (e inh)
+    fBinOp e1 op e2 inh = BinOp (e1 inh) op (e2 inh)
+    fInstanceOf e refType inh = InstanceOf (e inh) refType
+    fCond g e1 e2 inh = Cond (g inh) (e1 inh) (e2 inh)
+    fAssign lhs assOp e inh = Assign lhs assOp (e inh) -- TODO
+    fLambda lParams lExp _ = Lambda lParams lExp
+    fMethodRef className methodName _ = MethodRef className methodName
+ 
+-- | Desugars to a basic assignment, returning the new righ hand side. For example: desugaring x += 3 returns the new rhs x + 3
+desugarAssign :: Lhs -> AssignOp -> Exp -> Exp
+desugarAssign lhs op e = case op of
+                            EqualA -> e
+                            MultA -> BinOp e Mult (lhsToExp lhs)
+                            DivA -> BinOp e Div (lhsToExp lhs)
+                            RemA -> BinOp e Rem (lhsToExp lhs)
+                            AddA -> BinOp e Add (lhsToExp lhs)
+                            SubA -> BinOp e Sub (lhsToExp lhs)
+                            LShiftA -> BinOp e LShift (lhsToExp lhs)
+                            RShiftA -> BinOp e RShift (lhsToExp lhs)
+                            RRShiftA -> BinOp e RRShift (lhsToExp lhs)
+                            AndA -> BinOp e And (lhsToExp lhs)
+                            XorA -> BinOp e Xor (lhsToExp lhs)
+                            OrA -> BinOp e Or (lhsToExp lhs)
+    where 
+        lhsToExp (NameLhs name) = ExpName name
+        lhsToExp (FieldLhs fieldAccess) = undefined
+        lhsToExp (ArrayLhs arrayIndex) = undefined
+        
+-- | Substitutes all occurences of a specific free variable by an expression
+substVar :: Lhs -> Exp -> Exp -> Exp
+substVar lhs rhs e = foldExp substVarExpAlgebra e (lhs, rhs)
\ No newline at end of file