Hoare triple: Are those hoare triples are correct? Below there are some hoare triples. In the questions, either preconditions or postconditions are missed. I completed them under partial correctness. Are they correct?
a. (| ?? |) z=z+y-1; (| z >= y |)
   Answer: (| z > 0 |) z=z+y-1; (| z >= y |)

b. (| ?? |) x=x+1; (| x=y |)
   Answer: (| y = x + 1 |) x=x+1; (| x=y |)

c. (| a=9 |) a=2; b=a+1; a=b*b; (| ?? |)
   Answer: (| a=9 |) a=2; b=a+1; a=b*b; (| a > b |)

d. (| i=-j |) i=i+1; j=j-1; (| ?? |)
   Answer: (| i=-j |) i=i+1; j=j-1; (| y = |x| |)

e. (| ?? |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)
  Answer: (| z = 0 || z = 3 |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)

 A: The rule that (a) through (d) is presumably trying to invoke is:
$$\phi[e/v] ~;~ v := e ~;~ \phi$$
(where $A[B/C]$ means all occurences of $C$ are replaced by $B$ in $A$).  So for part (a), you have:
$$? ~;~ z := z + y - 1 ~;~ z \ge y$$
You know that $\phi$ is $z\ge y$, you know $v$ is $z$, and you know that $e$ is $z + y - 1$.  So you want to find
$$\phi[e/v] = (z \ge y)[z + y - 1 / z] = z + y - 1 \ge y$$
which is the same as $z > 0$, if you assume that we are dealing with integers, but maybe you aren't.
(b) should naturally be $x + 1 = y$, no reason to reverse it.  
For (c), $a > b$ isn't your strongest postcondition.  You should have $b = 3$, $a = 9$.  Just work through the computation directly.  This only works if you assume integers.
In part (d), you somehow managed to invoke variables $y$ and $x$ despite them not being part of the probem.  This one might be easier to just work forwards again (like in (c)) rather than try to apply the rules:
First you know $i = -j$.  Then you apply $i := i + 1$, so you can infer $i - 1 = -j$.  Then you apply $j = j - 1$.  So you can infer $(i - 1) = -(j + 1)$.  And this is only assuming you are dealing with a data structure where $+1$ and $-1$ are inverses.  You actually can't solve this problem otherwise.
For part (e), you want to invoke the rule:
$$\frac{[ B \land P ~;~ S ~;~ Q], [\lnot B \land P ~;~ T ~;~ Q]}{P ~;~ \text{if }B \text{ then }S\text{ else }T \text{ endif }~;~Q}$$
So $B$ is $z=0$, $S$ is $x=z+1$, $Q$ is $x=1$, and $T$ is $x=z-2$, and $P$ is unknown.  Filling in the blanks, that is:
$$\frac
{[ z=0 \land P ~;~ x=z+1 ~;~ x=1], [\lnot z=0 \land P ~;~ x=z-2 ~;~ x=1]}
{P ~;~ \text{if }z=0 \text{ then }x=z+1\text{ else }x = z-2 \text{ endif }~;~x=1}
$$
So what is the weakest $P$ that satsifies both $[ z=0 \land P ~;~ x=z+1 ~;~ x=1]$ and $[\lnot z=0 \land P ~;~ x=z-2 ~;~ x=1]$?  Use the same technique that was used in (a) through (d).  
!> The first condition is satisfied by $P=\top$.  The second is satisfied by $P = ((x = 1)[z - 2 / x])$ or $\lnot (\lnot z=0 \land P)$ which is $P = 0$.  So your answer here is correct.
