Solutions to Lab 8 exercises & Reflection

Written solutions

The written solutions for this week can be download as PDF below.

Download Solutions to Lab 8

Reflection

• You may have found the proof of the "Halting Problem" quite confusing... it is expected!

  There are several video animations trying to make you "see" the construction, and how the contradiction follows from the assumption that a decider exists.

  Find a few ones and choose your favourite.

• The "Halting Problem" is only the tip of the iceberg. Generally speaking, verifying that software does what it was designed to do is essentially undecidable too. However, this is a very important and critical area that we need in many mission critical software.

  Do your own research into how software verification is done in the "real world". Find concrete examples. Can we give up on being 100% and make some gains in terms of what we can verify?

Info

You don't have to hand-in your reflection -- this is not an assessment. Keep your notes and go over them as you understand the material more. Some of the above ideas will become clear in one week, while others will be met again towards the end of the module!