Recitation 05: Linear Search and Debugging

Linear Search

• Implementation
• 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.
• Variants:
  • 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]

Debugging

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 foo().

For these examples, some notes can be found in a comment at the top of the file.

• debugging1.c0 [sol]
• debugging2.c0
• debugging3.c0
• debugging4.c0

If you have any comments or see any errors, please let me know.