/*@
  @ ensures \result == \max( a, b );
  @ ensures \result != \min( a, b );
  @ ensures a == \abs( a );
  @*/
unsigned int
max( unsigned int a, unsigned int b )
{
	int i = a > b ? a : b;
	//@ assert i == \max( a, b );
	return i;
}