public /*@ pure @*/ int getNormalizationBias() {
        if (nWords == 0) {
            throw new IllegalArgumentException("Zero value cannot be normalized");
        }
        int zeros = Integer.numberOfLeadingZeros(data[nWords - 1]);
        return (zeros < 4) ? 28 + zeros : zeros - 4;
    }
public int getNormalizationBias ( ) { if ( nWords == 0 ) { throw new IllegalArgumentException ( "Zero value cannot be normalized" ) ; } int zeros = Integer . numberOfLeadingZeros ( data [ nWords - 1 ] ) ; return ( zeros < 4 ) ? 28 + zeros : zeros - 4 ; }
/*@
@ requires this.value() > 0;
@