add examples to show how BitTest is to be interpreted
fix incorect number of bits in postcondition