f a single trivial instruction
        <code class="computeroutput"><span class="special">++</span><span class="identifier">x</span></code>
        so it easy to check by visual inspection that it does not contain any bug
        and it will always increment <code class="computeroutput"><span class="identifier">x</span></code>
        by <code class="computeroutput"><span class="number">1</span></code> thus the function postcondition
        will never fail. In real code, function bodies are rarely this sim