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.