https://en.wikipedia.org/wiki/Formal_system

As a small example of using Hoare Logic, which takes every single command (aka line of code) in your program and turns it in to a Hoare Triple. A Hoare Triple looks like {precondition} command {postcondition}.

As an example let's prove the output is not 476.

    int numb;
    .....
    numb = numb * 2;  
    numb = numb + 1; 
    print numb

{numb = 476} print numb {We don't care what happens after you print}

If numb is 476 on the line above then the line before this one must have a post condition identical to this line's precondition.

{} numb = numb + 1; {numb = 476}

For this line to be true it must have a precondition that numb = 475

so {numb = 475} numb + 1; {numb = 476}

Again we chain this line's precondition to the previous line's post condition:

{} numb = numb * 2; {numb = 475}

Given that numb is defined as an integer there is no possible precondition capable of making this post condition true. We have formally proven this program is incapable of printing 476. Further since the stuff in the brackets can be as complex as we like we could have proven this program is incapable of printing even numbers.

https://en.wikipedia.org/wiki/Hoare_logic