Assignment 3

I am still wondering how to prove postcondition and termination.

In the question 4, I developed such program.

Function binSearch( x, A)

    b=0

    e = n – 1

    while ( b <= e )

    m = ( b + e ) // 2

    if (A[m] > x )

        e = m – 1

    else

        b = m + 1

return e

I tested it and got correct result base on professor’s example posted in piazza. But, I found it is very hard to prove loop invariant and postcondition. It is a little different of example of lecture. And professor did not show the entire proof.

If I modified code like this:

Function binSearch( x, A)

    b=0

e = n – 1

if ( x < A[0] )

    return -1

else if ( x >= A[n -1 ] )

    return n -1

else

        while ( b <= e )

        m = ( b + e ) // 2

        if (A[m] > x )

            e = m – 1

        else

            b = m + 1

    return e

This snippet seems to easier to prove one of postcondition that is -1<=p<=n-1. But, for my professional view, the former is more concise, the latter is more amateur.

Then, if I continued to make WHILE loop more bloated redundant, the proof would be easier and easier. As a professional developer, I could not accept such code like that. But….. how about my mark?

The solution has not been posted yet. I will check out professor’s answer.