diff --git a/col/src/main/java/vct/col/ast/print/AbstractPrinter.java b/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
index fb5152c33a..30fe8b2d2b 100644
--- a/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
@@ -10,12 +10,19 @@
 import vct.col.ast.generic.ASTNode;
 import vct.col.ast.stmt.composite.Hole;
 import vct.col.ast.stmt.decl.ASTSpecial;
+import vct.col.ast.stmt.decl.Contract;
+import vct.col.ast.stmt.decl.DeclarationStatement;
+import vct.col.ast.stmt.decl.SignalsClause;
 import vct.col.ast.type.ASTReserved;
 import vct.col.ast.type.PrimitiveType;
 import vct.col.ast.type.TypeExpression;
+import vct.col.ast.util.ASTUtils;
 import vct.col.ast.util.AbstractVisitor;
 import vct.col.ast.syntax.Syntax;
 
+import java.util.ArrayList;
+import java.util.List;
+
 /**
  * This class contains the generic code for pretty printing expressions
  * based on a given syntax.
@@ -251,5 +258,92 @@ public void visit(ASTSpecial s){
       break;
     }
   }
+
+  @Override
+  public void visit(Contract contract) {
+    if (contract!=null) {
+      for (DeclarationStatement d : contract.given) {
+        out.printf("given ");
+        d.accept(this);
+        out.lnprintf("");
+      }
+      for (ASTNode e : ASTUtils.conjuncts(contract.invariant, StandardOperator.Star)) {
+        out.printf("loop_invariant ");
+        nextExpr();
+        e.accept(this);
+        out.lnprintf(";");
+      }
+      List<ASTNode> contextElems = new ArrayList<>();
+      for (ASTNode pre : ASTUtils.conjuncts(contract.pre_condition, StandardOperator.Star)) {
+        boolean added = false;
+        for (ASTNode post : ASTUtils.conjuncts(contract.post_condition, StandardOperator.Star)) {
+          if (pre.equals(post)) {
+            contextElems.add(pre);
+            added = true;
+          }
+        }
+        if (!added) {
+          printContractElement(pre, "requires");
+        }
+      }
+      for (ASTNode con : contextElems) {
+        printContractElement(con, "context");
+      }
+      for (ASTNode post : ASTUtils.conjuncts(contract.post_condition, StandardOperator.Star)) {
+        if (!contextElems.contains(post)) {
+          printContractElement(post, "ensures");
+        }
+      }
+      for (DeclarationStatement d : contract.yields) {
+        out.printf("yields ");
+        d.accept(this);
+        out.lnprintf("");
+      }
+      for (SignalsClause sc : contract.signals) {
+        sc.accept(this);
+      }
+      if (contract.modifies != null) {
+        out.printf("modifies ");
+        if (contract.modifies.length == 0) {
+          out.lnprintf("\\nothing;");
+        } else {
+          nextExpr();
+          contract.modifies[0].accept(this);
+          for (int i = 1; i < contract.modifies.length; i++) {
+            out.printf(", ");
+            nextExpr();
+            contract.modifies[i].accept(this);
+          }
+          out.lnprintf(";");
+        }
+      }
+      if (contract.accesses != null) {
+        out.printf("accessible ");
+        if (contract.accesses.length == 0) {
+          out.lnprintf("\\nothing;");
+        } else {
+          nextExpr();
+          contract.accesses[0].accept(this);
+          for (int i = 1; i < contract.accesses.length; i++) {
+            out.printf(", ");
+            nextExpr();
+            contract.accesses[i].accept(this);
+          }
+          out.lnprintf(";");
+        }
+      }
+    }
+  }
+
+  protected void printContractElement(ASTNode expr, String contractHead) {
+    out.printf(contractHead + " ");
+    nextExpr();
+    if(expr instanceof MethodInvokation)
+      out.print("(");
+    expr.accept(this);
+    if(expr instanceof MethodInvokation)
+      out.print(")");
+    out.lnprintf(";");
+  }
 }
 
diff --git a/col/src/main/java/vct/col/ast/print/JavaPrinter.java b/col/src/main/java/vct/col/ast/print/JavaPrinter.java
index 3c6904d92c..67ab8072b2 100644
--- a/col/src/main/java/vct/col/ast/print/JavaPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/JavaPrinter.java
@@ -25,7 +25,6 @@
 import vct.col.ast.type.*;
 import vct.col.ast.syntax.JavaDialect;
 import vct.col.ast.syntax.JavaSyntax;
-import vct.col.ast.util.ASTUtils;
 import vct.col.ast.util.ClassName;
 import hre.util.LambdaHelper;
 
@@ -632,67 +631,7 @@ public void visit(Contract contract) {
     if (contract!=null){
       out.lnprintf("/*@");
       out.incrIndent();
-      for (DeclarationStatement d:contract.given){
-        out.printf("given ");
-        d.accept(this);
-        out.lnprintf("");
-      }
-      for(ASTNode e:ASTUtils.conjuncts(contract.invariant,StandardOperator.Star)){
-        out.printf("loop_invariant ");
-        nextExpr();
-        e.accept(this);
-        out.lnprintf(";");
-      }
-      for(ASTNode e:ASTUtils.conjuncts(contract.pre_condition,StandardOperator.Star)){
-        out.printf("requires ");
-        nextExpr();
-        e.accept(this);
-        out.lnprintf(";");
-      }
-      for (DeclarationStatement d:contract.yields){
-        out.printf("yields ");
-        d.accept(this);
-        out.lnprintf("");
-      }
-      for(ASTNode e:ASTUtils.conjuncts(contract.post_condition,StandardOperator.Star)){
-        out.printf("ensures ");
-        nextExpr();
-        e.accept(this);
-        out.lnprintf(";");
-      }
-      for (SignalsClause sc : contract.signals){
-        sc.accept(this);
-      }
-      if (contract.modifies!=null){
-        out.printf("modifies ");
-        if (contract.modifies.length==0){
-          out.lnprintf("\\nothing;");
-        } else {
-          nextExpr();
-          contract.modifies[0].accept(this);
-          for(int i=1;i<contract.modifies.length;i++){
-            out.printf(", ");
-            nextExpr();
-            contract.modifies[i].accept(this);
-          }
-          out.lnprintf(";");
-        }
-      }
-      if (contract.accesses!=null){
-        out.printf("accessible ");
-        if (contract.accesses.length==0){
-          out.lnprintf("\\nothing;");
-        } else {
-          nextExpr();
-          contract.accesses[0].accept(this);
-          for(int i=1;i<contract.accesses.length;i++){
-            out.printf(", ");
-            nextExpr();
-            contract.accesses[i].accept(this);
-          }
-          out.lnprintf(";");
-        }
-      }
+      super.visit(contract);
       out.decrIndent();
       out.lnprintf("@*/");
     }
@@ -1439,17 +1378,17 @@ public void visit(VariableDeclaration decl){
       sep=",";
       if (dd instanceof DeclarationStatement){
         DeclarationStatement d = (DeclarationStatement)dd;
-        d.getType().accept(this);
+        out.print(d.name());
         ASTNode init = d.initJava();
         if (init!=null){
-          out.print("=");
+          out.print(" = ");
+          setExpr();
           init.accept(this);
         }
       } else {
         out.print("TODO");
       }
     }
-    out.println(";");
   }
   
   @Override
diff --git a/col/src/main/java/vct/col/ast/print/PVLPrinter.java b/col/src/main/java/vct/col/ast/print/PVLPrinter.java
index da9fe97eca..903429dc42 100644
--- a/col/src/main/java/vct/col/ast/print/PVLPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/PVLPrinter.java
@@ -18,13 +18,11 @@
 import vct.col.ast.stmt.terminal.ReturnStatement;
 import vct.col.ast.syntax.JavaDialect;
 import vct.col.ast.syntax.PVLSyntax;
-import vct.col.ast.syntax.Syntax;
 import vct.col.ast.type.*;
-import vct.col.ast.util.ASTUtils;
 import vct.col.ast.util.ClassName;
 
 import java.io.PrintWriter;
-import java.util.List;
+import java.util.*;
 
 import static hre.lang.System.DebugException;
 
@@ -53,9 +51,11 @@ public void pre_visit(ASTNode node){
             if (ann==null){
                 out.printf(" <null annotation> ");
             } else {
-                nextExpr();
-                ann.accept(this);
-                out.printf(" ");
+                if(!(node instanceof Method && ((Method)node).kind == Method.Kind.Pure)) {
+                    nextExpr();
+                    ann.accept(this);
+                    out.printf(" ");
+                }
             }
         }
     }
@@ -281,6 +281,7 @@ public void visit(ASTSpecial s){
                 setExpr();
                 ASTNode prop=s.args[0];
                 prop.accept(this);
+                out.println(";");
                 break;
             }
             case Join:{
@@ -289,6 +290,7 @@ public void visit(ASTSpecial s){
                 setExpr();
                 ASTNode prop=s.args[0];
                 prop.accept(this);
+                out.println(";");
                 break;
             }
             case Goto:
@@ -537,18 +539,12 @@ public void visit(BlockStatement block){
         int N=block.getLength();
         for(int i=0;i<N;i++){
             ASTNode statement=block.getStatement(i);
-            if (statement.isValidFlag(ASTFlags.GHOST) && statement.isGhost()){
-                out.enterGhost();
-            }
             statement.accept(this);
             if (self_terminating(statement)){
                 out.clearline();
             } else {
                 out.lnprintf(";");
             }
-            if (statement.isValidFlag(ASTFlags.GHOST) && statement.isGhost()){
-                out.leaveGhost();
-            }
         }
         out.decrIndent();
         out.printf("}");
@@ -582,75 +578,6 @@ public void visit(ASTClass cl){
         out.println("");
     }
 
-    @Override
-    public void visit(Contract contract) {
-        if (contract!=null){
-            //out.incrIndent();
-            for (DeclarationStatement d:contract.given){
-                out.printf("given ");
-                d.accept(this);
-                out.lnprintf("");
-            }
-            for(ASTNode e:ASTUtils.conjuncts(contract.invariant,StandardOperator.Star)){
-                out.printf("loop_invariant ");
-                nextExpr();
-                e.accept(this);
-                out.lnprintf(";");
-            }
-            for(ASTNode e:ASTUtils.conjuncts(contract.pre_condition,StandardOperator.Star)){
-                out.printf("requires ");
-                nextExpr();
-                e.accept(this);
-                out.lnprintf(";");
-            }
-            for (DeclarationStatement d:contract.yields){
-                out.printf("yields ");
-                d.accept(this);
-                out.lnprintf("");
-            }
-            for(ASTNode e:ASTUtils.conjuncts(contract.post_condition,StandardOperator.Star)){
-                out.printf("ensures ");
-                nextExpr();
-                e.accept(this);
-                out.lnprintf(";");
-            }
-            for (SignalsClause sc : contract.signals){
-                sc.accept(this);
-            }
-            if (contract.modifies!=null){
-                out.printf("modifies ");
-                if (contract.modifies.length==0){
-                    out.lnprintf("\\nothing;");
-                } else {
-                    nextExpr();
-                    contract.modifies[0].accept(this);
-                    for(int i=1;i<contract.modifies.length;i++){
-                        out.printf(", ");
-                        nextExpr();
-                        contract.modifies[i].accept(this);
-                    }
-                    out.lnprintf(";");
-                }
-            }
-            if (contract.accesses!=null){
-                out.printf("accessible ");
-                if (contract.accesses.length==0){
-                    out.lnprintf("\\nothing;");
-                } else {
-                    nextExpr();
-                    contract.accesses[0].accept(this);
-                    for(int i=1;i<contract.accesses.length;i++){
-                        out.printf(", ");
-                        nextExpr();
-                        contract.accesses[i].accept(this);
-                    }
-                    out.lnprintf(";");
-                }
-            }
-            //out.decrIndent();
-        }
-    }
-
     public void visit(SignalsClause sc) {
         out.printf("signals (");
         sc.type().accept(this);
@@ -679,13 +606,8 @@ public void visit(Method m){
         String name=m.getName();
         Contract contract=m.getContract();
         boolean predicate=m.getKind()==Method.Kind.Predicate;
-        if (predicate){
-            if (contract!=null) {
-                out.lnprintf("//ignoring contract of predicate");
+        if (predicate && contract!=null){
                 Debug("ignoring contract of predicate");
-            }
-            out.incrIndent();
-            out.print("predicate ");
         }
         if (contract!=null && !predicate){
             visit(contract);
@@ -700,7 +622,7 @@ public void visit(Method m){
                         case ASTFlags.INLINE:
                             out.printf("inline ");
                         case ASTFlags.PUBLIC:
-                            out.printf("public ");
+                            //no public in PVL
                             break;
                         case ASTFlags.THREAD_LOCAL:
                             out.printf("thread_local  ");
@@ -732,9 +654,6 @@ public void visit(Method m){
             result_type.accept(this);
             out.printf(" ");
         }
-        if (m.getKind()==Method.Kind.Pure) {
-            out.printf("pure ");
-        }
         out.printf("%s(",name);
         if (N>0) {
             DeclarationStatement args[]=m.getArgs();
@@ -780,9 +699,6 @@ public void visit(Method m){
             body.accept(this);
             out.lnprintf(";");
         }
-        if (predicate){
-            out.decrIndent();
-        }
     }
 
     public void visit(IfStatement s){
@@ -1285,9 +1201,12 @@ public void visit(ParallelRegion region){
         } else {
             out.println("par");
         }
-        for (ParallelBlock pb : region.blocksJava()) {
+        for (Iterator<ParallelBlock> it = region.blocksJava().iterator(); it.hasNext();) {
             out.incrIndent();
-            pb.accept(this);
+            it.next().accept(this);
+            if(it.hasNext()) {
+                out.print(" and");
+            }
             out.println("");
             out.decrIndent();
         }
@@ -1310,17 +1229,17 @@ public void visit(VariableDeclaration decl){
             sep=",";
             if (dd instanceof DeclarationStatement){
                 DeclarationStatement d = (DeclarationStatement)dd;
-                d.getType().accept(this);
+                out.print(d.name());
                 ASTNode init = d.initJava();
                 if (init!=null){
-                    out.print("=");
+                    out.print(" = ");
+                    setExpr();
                     init.accept(this);
                 }
             } else {
                 out.print("TODO");
             }
         }
-        out.println(";");
     }
 
     @Override
diff --git a/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java b/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
index 2c4542069d..f822a28893 100644
--- a/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
+++ b/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
@@ -12,11 +12,7 @@
 import java.io.PrintWriter;
 
 import static vct.col.ast.expr.StandardOperator.*;
-import static vct.col.ast.type.ASTReserved.FullPerm;
-import static vct.col.ast.type.ASTReserved.NoPerm;
-import static vct.col.ast.type.ASTReserved.ReadPerm;
-import static vct.col.ast.type.ASTReserved.EmptyProcess;
-import static vct.col.ast.type.ASTReserved.CurrentThread;
+import static vct.col.ast.type.ASTReserved.*;
 
 /**
  * Defines the syntax of common types and operations of  
@@ -38,7 +34,8 @@ public static PVLSyntax get(){
       syntax=new PVLSyntax("PVL");
 
       VerCorsSyntax.add(syntax);
-      
+      syntax.addPostfix(PostIncr,"++",140);
+      syntax.addPostfix(PostDecr,"--",140);
       //syntax.addInfix(SubType,"<:",90);
       //syntax.addInfix(SuperType,":>",90);
       syntax.addInfix(Implies,"==>",30);
@@ -177,6 +174,8 @@ public static PVLSyntax get(){
       syntax.addReserved(NoPerm,"none");
       syntax.addReserved(EmptyProcess,"empty");
       syntax.addReserved(CurrentThread,"current_thread");
+      syntax.addReserved(Null,"null");
+      syntax.addReserved(This,"this");
       
       syntax.addOperator(Unfolding,140,"unfolding","in","");