How to determine the pre and post conditions of a program (Hoare-logic) Problem
Below is a program named X:
y = 1;
while(y &lt; x){
    y = 10 * y;
}

What does this program X do? What are appropriate pre and post conditions?
 (Assume that x and y are integers).

My solution
Given a whole number x &gt; 1, X should give us a power of 10 greater than or equal to x.
pre-condition: (|x = x0 ∧ x0 &gt; 1|)
post-condition: (|y ≥ x ∧ ∃n(y=10n)|)
However, I don't know if my solution is correct. It would be nice to know how to solve this trivial problem.
Here are two other programs that have the same postcondition given the same precondition:
y = 1;
while (y &lt; x) {
    y = 100 * y;
}

x = y = 1;

Your postcondition doesn't describe the output it enough detail. In particular:

The program doesn't change $x$.
The value of $y$ is the smallest power of 10 which is at least $x$.