s="number">1</span></code> without
      overflowing). The postcondition states that at function exit the argument
      <code class="computeroutput"><span class="identifier">x</span></code> must be incremented by <code class="computeroutput"><span class="number">1</span></code> with respect to the <span class="emphasis"><em>old value</em></span>
      that <code class="computeroutput"><span class="identifier">x</span></code> had before executing
      the function (indicated here by <code class="literal"><