Recitation 05: Linear Search and Debugging
- Pay attention to the is_in() function, since we'll be using
it in our annotations.
- As an activity to better understand how contracts work together, we
can examine how contracts lead to one another. If we number our contracts
as shown here.
We can draw arrows connecting these contracts, as follows:
1 --> 2 --> 8
3 --> 6
4 --> 7
5 --> 6
- Exercise: now write out the proof, using this as a roadmap.
- What if the list is sorted? How can we change the code and
strengthen our contracts to take advantage of this? [code]
- What if we want to find the index of the last occurance of the
element instad of the first occurance? Change the code accordingly. [code]
Before we get to debugging, remember that a little extra work up front
can save you a lot of time and frustration in the long run. Test and debug
incrementally. So, after you write a function, test it to make sure
everything works as expected. It'll be a lot easier to find that bug in
foo() than later when the bug happens once bar() calls
For these examples, some notes can be found in a comment at the top of
If you have any comments or see any errors, please
let me know.