postconditions:level(low),not level(high)