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

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.

• We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher.
– D.W.
Jan 6, 2021 at 19:38

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$$.