Verifying the precedence property pattern using the B Method