How to determine the pre and post conditions of a program (Hoare-logic)

Question

Problem
Below is a program named X:

y = 1;
while(y < 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 > 1, X should give us a power of 10 greater than or equal to x.
pre-condition: (|x = x0 ∧ x0 > 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.

Answer 1

Here are two other programs that have the same postcondition given the same precondition:

y = 1;
while (y < 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$.