Informal Methods - Autumn 2018


Welcome to Informal Methods in 2018.

This course is intended to sharpen your skills in writing correct, yet fast code.  You will not be tested on your knowledge of the theory underlying the formal techniques we'll study (there is no exam), but rather your ability to apply them in practice.  As such, the course will run as an interactive seminar - you will be graded on class participation (10%).  Attendance is essential - you cannot pass this course by following the reading material.  Likewise, participation and attention is also mandatory - this means: laptops closed, mobile phones away, and absolutely no watching of Game of Thrones on Google Glass.

You'll be working to build your "muscle memory" - like a pianist playing scales, you will learn to derive and use invariants, reason statically, without going back to basic principles, or looking it up in a textbook.  Therefore, the most important thing of all is practice: We will work through examples in the lectures, as a group; I will also provide exercises to work through in your own time.  I cannot emphasise too strongly that the only way to get really good is to invest the time and practice.


The assessment for this course consists of 3 written assignments.  There will be no exam.  The assignments will be collected in Moodle, and I am planning to release the first at the end of week 3.  Late submissions will be penalised by reducing the maximum possible mark by 10% per day i.e. a 3-day-late submission can score a maximum of 70%.

Update 27/9: You can now submit your completed homework exercises (as PDFs) via Moodle.

Update 18/10: There was an error in the binary search annotation in the week 3 lecture notes.  The updated version is now linked.

Important Links

  • Moodle course - enrolled students only, nethz username & password.  We'll use the Moodle instance to distribute materials (readings, homework etc.) and to manage assignment submissions.

Weekly Summary

  • Week 1: We began with a brief exercise on binary search.  We spent the rest of the lecture discussing the Zune date bug, and how to use flowcharts and annotations to both detect and correct the problem.  Homework exercises on flowchart annotation are on moodle.
  • Week 2: We began by showing termination of the fixed Zune algorithm by using a variant.  We then carefully derived an algorithm to find the maximum element of an array.  This forced us to think carefully about the maximum of an empty set.  We then derived the Hoare triples for assignment, if and loops from their flowchart equivalents.  We began on the maximum subsequence sum.  Homework is on max/min/lub.
  • Week 3: We finished the max-subsegment-sum program by adding an auxiliary variable and invariant, giving an O(n) solution.  We then revisited binary search with a class exercise, showing both correctness and termination.  Homework is to write a binary insertion sort, using our binary search as a subroutine.
  • Week 4: We spent the whole lecture on the maximal increasing subsequence problem, which forms the core of the first assignment, due in week 6.
  • Week 5: In the first half of the lecture we derived an algorithm for log-time exponentiation, using a tail invariant.  In the second hour we tried to adapt our binary search/sorting algorithms to sort lists downward, just by changing the comparison operator.  We started thinking about whether we could say that this program is equivalent to the alternative of sorting and then reversing the list.  Homework is to play around with an implementation of these parameterised algorithms.
  • Week 6: We completed our parametric sorting function, taking the comparison as an argument.  We then played around with different comparison functions, showing that a stricter comparison leads to a program refinement.  We then introduced data refinement, and used it to remove the sentinels from an external insertion sort.  We started looking at using data refinement to write a selection sort, which we'll use to turn it into heapsort.
  • Week 7:  We implemented the pop() function (for selection sort) using a list, and showed its correctness using an interpretation function.  We discussed the link between data refinement and object-oriented programming.  Homework is to revisit downward sorting using data refinement, and read a paper by Wirth.
  • Week 8: I gave some feedback on the first assignment, emphasising that the most important skill for this course is the ability to communicate your results clearly.  We then finished our derivation and proof of the heap-based pop() function, turning our selection sort into a heapsort.  Homework is to read a paper by Dijkstra, covering the longest upsequence algorithm.
  • Week 9:  We had a guest lecture from Tom Sewell (ex of NICTA, now Chalmers) on the techniques used to verify the seL4 microkernel.   An article in a recent issue of CACM gives some more detail on the helicopter example Tom presented.
  • Week 10:  We worked through the derivation of Dijkstra's shortest path algorithm as an amoeba race.  We got as far as the the first data refinement (to remove the amoebae), having settled on an invariant - the rest of the development is in the lecture notes.  This algorithm is the core of assignment 2, which I released this week (due Wednesday of week 12).
  • Week 11: We started a new topic: Owicki-Gries reasoning for parallel programs.  We started by relating static assertions (on programs) to dynamic assertions (on traces).  We started on implementing a mutex, and the remainder is a homework exercise.
  • Week 12: This week we completed the proof of our mutex, and discussed how to use it to simplify Owicki-Gries reasoning within critical sections (derive a contradiction from 'A holds mutex', 'B holds mutex' & the invariant).
  • Week 13: We developed a bounded-buffer producer-consumer queue in class, found an interpretation + invariant (streams), and got as far as showing local correctness.  This will form the basis for assignment 3, released in week 14.


  • Thursday 10-12, ETHZ CAB G 56