In our previous work we have studied several coinductive operational semantics, all of which are proved equivalent, for the While language to describe terminating as well as non-terminating program executions. The operational semantics keep track of all the intermediate states that an execution goes through as a trace (a sequence of states). The trace is finite for a terminating execution and infinite for a non-terminating execution. In this talk I present a Hoare-logic for While, which is proved sound and complete with respect to those operational semantics. As usual, our Hoare-triple consists of a precondition, a statement and a postcondition. The precondition is a predicate on initial states, whereas the postcondition is a predicate on traces. Since a trace contains the full information about an execution, the logic can talk about for instance if an execution is terminating or if an variable is updated infinitely often. My talk will start by introducing a coinductive big-step relational semantics, then present the Hoare-logic. I will explain some interesting design issues on the logic and our strategy for proving its completeness, that we have discovered through many failed attempts. All the results have been formalized in Coq. This is a joint work with Tarmo Uustalu.