WLP Transformer implementation in Java?

Input for our program is array of instructions (Expression [] instructions). Then iteratively starting from last instruction, and going backwards we searching for weakest pre-condition of single instruction.

First (last in array) instruction has post-condition {true}. Then next instruction has post-condition equal to wlp (weakest liberal precondition) of previous instruction. Wlp of last instruction (first in array) is the wlp of whole program.

Finding wlp of single binary operation will look like that:

public Wlp findWlpForBinaryExp(BinaryExp, Expresion [] post) {
      //code
      switch(BinaryExp.operator) {
          case '+':
              //...
          case '-':
              //...
          //...
      }
   }

But in fact value of variable doesn’t change in operations ‘+’, or, ‘-’. it changes only when there is ‘=’ operator (so assignment). So should we ignore expressions where is only ‘+’ sign? Or, how can we glue a few expressions? Because instruction: x = a + 3; is not one, but two expressions, right?

Maybe this Q[e/x] we could implement it in that way:

public Wlp findWlpForQex(Literal x, Expresion [] post) {

Literal e = new Literal();   
e=x;    // ???
}

I still not sure about this Q[e/x], and also I'm not sure how to process whole input? Iteratively through instructions, or through binary operations?

In general, this is what we have so far:

class WlpTransformer {
    Expression [] instructions;     // or some additional class GlcObject


    public Wlp findWlpForBinaryExp(BinaryExp be, Wlp postConditions) {
        //code
        switch(be.operator) {
            case '+':
                //...
            case '-':
                //...
            //...
        }
    }

    public Wlp findWlpForSkip(Expression e, Wlp postConditions) {
        return postConditions;

    }

}

class Wlp
{
    Expression [] preconditions;

}

How we should implement this?