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.


closed as too broad by Raphael Dec 10 '17 at 19:47

Please edit the question to limit it to a specific problem with enough detail to identify an adequate answer. Avoid asking multiple distinct questions at once. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ 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 $\endgroup$ – Raphael Dec 10 '17 at 19:52
  • $\begingroup$ @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. $\endgroup$ – Roboticist Dec 10 '17 at 19:56
  • 1
    $\begingroup$ "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. $\endgroup$ – D.W. Dec 10 '17 at 20:21
  • 2
    $\begingroup$ Since you are asking for the best practice method, can you comment on what methods you are familiar with? e.g. loop invariants $\endgroup$ – JimN Dec 10 '17 at 21:28

Browse other questions tagged or ask your own question.