How to write a theorem corresponding to an algorithm's proof of correctness? [closed]

Let $X$ be an algorithm whose correctness supposed to be proved. What is the best practice to write the corresponding theorem?

For example:

Theorem: Algorithm $X$ correctly computes its output.

• This question is wayyyy too broad. There may be a reference question we should write here, but it may be a better idea to split into more specific parts. Examples: cs.stackexchange.com/q/59964/98 cs.stackexchange.com/q/2152/98. Of related interest: cs.stackexchange.com/q/29475/98 cs.stackexchange.com/q/13785/98 Commented Dec 10, 2017 at 19:52
• @Raphael: Thanks, but the question is not about the procedure to prove the correctness of an algorithm, but how one should verbally compose the theorem which reflects that correctness! My example does not seem to be so professional and mathematically fluent and standard.
– user33772
Commented Dec 10, 2017 at 19:56
• "Best practice" is subjective / a matter of opinion, which isn't a good fit here; see our help center. What exactly is your question? In general the answer is you write a specification of what it means for the algorithm to be correct, then you state the claim that the algorithm meets this specification. I find it hard to imagine that this is the kind of answer you are looking for, but it's hard for me to know what you are looking for. Perhaps if you've done some research or considered some possible answers and rejected them it would help if you told us why you rejected them.
– D.W.
Commented Dec 10, 2017 at 20:21
• Since you are asking for the best practice method, can you comment on what methods you are familiar with? e.g. loop invariants
– JimN
Commented Dec 10, 2017 at 21:28