questions about hw5 (copy from KLMS)

[yuanchunHE]

Questions

The hw document says max_heapify() will guarantee the result subtree with root=i a max heap. Does it mean the result tree might not be a perfect max heap? do we need to deal with this situation?

And would you give some hint about the proof of a sufficient unwinding number?

Answered by professor

-> The hw document says max_heapify() will guarantee the result sub tree with root=i a max heap. Yes

->Does it mean the result tree might not be a perfect max heap? do we need to deal with this situation? You are right. Even after max_heapify(...i...), i's parent node may still violate a max heap property. Your assertions should address such cases too.

-> would you give some hint about the proof of a sufficient unwinding number?

1. You can write down your rationale to support your own unwinding number. And/or
2. You can increase a unwinding number from 2 to N where the verification w/ unwinding # 2 to N-1 did not detect a (intentionally inserted or genuine) violation but the verification w/ N did.

Further Discussion

Student, So, in this case, what we supposed to do covers (1)testing functionalities of target module and (2)ensuring a right situation to call this module. However, in my view, (2) will surely be tested in another level/part of testing, and this point seems to be double checked. Is it really necessary from the perspective of testing?

Professor, -> 2) ... really necessary from the perspective of testing? Yes, 2) is necessary since a buggy implementation of max_heapify (...i...) may read ancestors of i and such bug may be revealed only through specific configuration of i's ancestors. That is why you should provide as general input space as possible.

[yuanchunHE]

>(2)ensuring a right situation to call this module, By (2), what I was asking is that do we need to ensure that the input to 'max_heapify()' ensures that the result is a perfect max heap (such as adding 'CPROVERassume()' as input space constraints). But your answer was 'yes...should provide as general input space as possible'. Sorry, I think I didn't clearly show my point, and there might be some misunderstanding...

Through your other answers, I guess what you meant is that we should provide a very general input, which might cause a not perfect max heap result, for max_heapify(), AND we should check whether the entire result is a perfect max heap. Is my guess correct?

[ahcheongL]

we should check whether the entire result is a perfect max heap

We don't check the entire result is a perfect max heap here because max_heapify(x, i, h_size) function works on only subtree of given x[i].

You have to check the other parts of the tree stay the same after the execution of the function.

(2) surely be tested in another level/part of testing ... really necessary from the perspective of testing?

One weak point of testing is that we are NOT sure that it can be detected by testing. The bug might "be revealed through only specific complex configuration", and testing techniques can't assure that they can generate tests to trigger such complex conditions.