Formal annotating Code for Optimizations?

[Manfred_Nowak]

Example:
If two actions `a1',`a2' are based on a binary decision `b' then on a 
pure logical level one can code:

  if( b)
    a1.do; // actions have `do'- and `undo'-methods
  else
    a2.do; 

But if one knows, that the probability of `b' to be `true' is much 
greater than .5, then in order to use the precomputing capabilities 
of the CPU one would probably like to code:

  a1.do;
  if( !b){
    a1.undo;
    a2.do;
  }    
    
The other case requires similar code.

In this latter code the abstraction of a simple binary decision seems 
to be less obvious, which seems to be bad for maintenance.

Of course one can annotate with comments. But since comments can be 
hints for defencies in the language, the question rises whether one 
should formalize this:

  if( b)note( p(b)>.8)
    a1.do;
    undo a1.undo;
  else
    a2;
    undo a2.undo;

-manfred
-- 
Maybe some knowledge of some types of disagreeing and their relation 
can turn out to be useful:
http://blog.createdebate.com/2008/04/07/writing-strong-arguments/