A variant of the while loop is the do-while loop which executes the statements in the while loop first and then check for the condition. Formally given as: do-while(B) Combine the existing proof rules in hoare logic to infer the pre and post conditions for do-while loop program construct. A variant of the while loop is the do-while loop which executes the statements in the while loop first and then check for the condition. Formally given as: do-while(B) Combine the existing proof rules in hoare logic to infer the pre and post conditions for do-while loop program construct