notebooks/Assertions.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "# Asserting Expectations\n",
    "\n",
    "In the previous chapters on [tracing](Tracer.ipynb) and [interactive debugging](Debugger.ipynb), we have seen how to observe executions. By checking our observations against our expectations, we can find out when and how the program state is faulty. So far, we have assumed that this check would be done by _humans_ – that is, us. However, having this check done by a _computer_, for instance as part of the execution, is infinitely more rigorous and efficient. In this chapter, we introduce techniques to _specify_ our expectations and to check them at runtime, enabling us to detect faults _right as they occur_."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from bookutils import YouTubeVideo\n",
    "YouTubeVideo(\"9mI9sbKFkwU\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "**Prerequisites**\n",
    "\n",
    "* You should have read the [chapter on tracing executions](Tracer.ipynb)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    },
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "outputs": [],
   "source": [
    "import bookutils.setup"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from bookutils import quiz"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import Tracer"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    }
   },
   "source": [
    "## Synopsis\n",
    "<!-- Automatically generated. Do not edit. -->\n",
    "\n",
    "To [use the code provided in this chapter](Importing.ipynb), write\n",
    "\n",
    "```python\n",
    ">>> from debuggingbook.Assertions import <identifier>\n",
    "```\n",
    "\n",
    "and then make use of the following features.\n",
    "\n",
    "\n",
    "This chapter discusses _assertions_ to define _assumptions_ on function inputs and results:\n",
    "\n",
    "```python\n",
    ">>> def my_square_root(x):  # type: ignore\n",
    ">>>     assert x >= 0\n",
    ">>>     y = square_root(x)\n",
    ">>>     assert math.isclose(y * y, x)\n",
    ">>>     return y\n",
    "```\n",
    "Notably, assertions detect _violations_ of these assumptions at runtime:\n",
    "\n",
    "```python\n",
    ">>> with ExpectError():\n",
    ">>>     y = my_square_root(-1)\n",
    "Traceback (most recent call last):\n",
    "  File \"<ipython-input-158-b63177b4c2f7>\", line 2, in <module>\n",
    "    y = my_square_root(-1)\n",
    "  File \"<ipython-input-157-dc1d0082e740>\", line 2, in my_square_root\n",
    "    assert x >= 0\n",
    "AssertionError (expected)\n",
    "\n",
    "```\n",
    "_System assertions_ help to detect invalid memory operations.\n",
    "\n",
    "```python\n",
    ">>> managed_mem = ManagedMemory()\n",
    ">>> managed_mem\n",
    "```\n",
    "|Address|<span style=\"color: blue\">0</span>|<span style=\"color: blue\">1</span>|<span style=\"color: lightgrey\">2</span>|<span style=\"color: lightgrey\">3</span>|<span style=\"color: lightgrey\">4</span>|<span style=\"color: lightgrey\">5</span>|<span style=\"color: lightgrey\">6</span>|<span style=\"color: lightgrey\">7</span>|<span style=\"color: lightgrey\">8</span>|<span style=\"color: lightgrey\">9</span>|\n",
    "|:---|:---|:---|:---|:---|:---|:---|:---|:---|:---|:---|\n",
    "|Allocated| | | | | | | | | | |\n",
    "|Initialized| | | | | | | | | | |\n",
    "|Content|-1|0| | | | | | | | |\n",
    "\n",
    "```\n",
    ">>> with ExpectError():\n",
    ">>>     x = managed_mem[2]\n",
    "Traceback (most recent call last):\n",
    "  File \"<ipython-input-160-89a206319ebb>\", line 2, in <module>\n",
    "    x = managed_mem[2]\n",
    "  File \"<ipython-input-97-d25e50073b38>\", line 3, in __getitem__\n",
    "    return self.read(address)\n",
    "  File \"<ipython-input-138-7b46abe4a8e1>\", line 10, in read\n",
    "    \"Reading from unallocated memory\"\n",
    "AssertionError: Reading from unallocated memory (expected)\n",
    "\n",
    "```\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Introducing Assertions\n",
    "\n",
    "[Tracers](Tracer.ipynb) and [Interactive Debuggers](Debugger.ipynb) are very flexible tools that allow you to observe precisely what happens during a program execution. It is still _you_, however, who has to check program states and traces against your expectations. There is nothing wrong with that – except that checking hundreds of statements or variables can quickly become a pretty boring and tedious task.\n",
    "\n",
    "Processing and checking large amounts of data is actually precisely what _computers were invented for_. Hence, we should aim to _delegate such checking tasks to our computers_ as much as we can. This automates another essential part of debugging – maybe even _the_ most essential part."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Assertions\n",
    "\n",
    "The standard tool for having the computer check specific conditions at runtime is called an _assertion_. An assertion takes the form\n",
    "\n",
    "```python\n",
    "assert condition\n",
    "```\n",
    "\n",
    "and states that, at runtime, the computer should check that `condition` holds, e.g. evaluates to True. If the condition holds, then nothing happens:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "assert True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If the condition evaluates to _False_, however, then the assertion _fails_, indicating an internal error."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ExpectError import ExpectError"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    assert False"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A common usage for assertions is for _testing_. For instance, we can test a square root function as"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def test_square_root() -> None:\n",
    "    assert square_root(4) == 2\n",
    "    assert square_root(9) == 3\n",
    "    ..."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "and `test_square_root()` will fail if `square_root()` returns a wrong value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Assertions are available in all programming languages. You can even go and implement assertions yourself:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def my_own_assert(cond: bool) -> None:\n",
    "    if not cond:\n",
    "        raise AssertionError"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "... and get (almost) the same functionality:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    my_own_assert(2 + 2 == 5)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Assertion Diagnostics"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In most languages, _built-in assertions_ offer a bit more functionality than what can be obtained with self-defined functions. Most notably, built-in assertions \n",
    "\n",
    "* frequently tell _which condition_ failed (`2 + 2 == 5`)\n",
    "* frequently tell _where_ the assertion failed (`line 2`), and\n",
    "* are _optional_ – that is, they can be turned off to save computation time."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "C and C++, for instance, provide an `assert()` function that does all this:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "open('testassert.c', 'w').write(r'''\n",
    "#include <stdio.h>\n",
    "#include \"assert.h\"\n",
    "\n",
    "int main(int argc, char *argv[]) {\n",
    "    assert(2 + 2 == 5);\n",
    "    printf(\"Foo\\n\");\n",
    "}\n",
    "''');"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "from bookutils import print_content"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('testassert.c').read(), '.h')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we compile this function and execute it, the assertion (expectedly) fails:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -g -o testassert testassert.c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testassert"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "How would the C `assert()` function be able to report the condition and the current location? In fact, `assert()` is commonly implemented as a _macro_ that besides checking the condition, also turns it into a _string_ for a potential error message. Additional macros such as `__FILE__` and `__LINE__` expand into the current location and line, which can then all be used in the assertion error message."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A very simple definition of `assert()` that provides the above diagnostics looks like this:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "open('assert.h', 'w').write(r'''\n",
    "#include <stdio.h>\n",
    "#include <stdlib.h>\n",
    "\n",
    "#ifndef NDEBUG\n",
    "#define assert(cond) \\\n",
    "    if (!(cond)) { \\\n",
    "        fprintf(stderr, \"Assertion failed: %s, function %s, file %s, line %d\", \\\n",
    "            #cond, __func__, __FILE__, __LINE__); \\\n",
    "        exit(1); \\\n",
    "    }\n",
    "#else\n",
    "#define assert(cond) ((void) 0)\n",
    "#endif\n",
    "''');"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('assert.h').read(), '.h')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "(If you think that this is cryptic, you should have a look at an [_actual_ `<assert.h>` header file](https://github.com/bminor/glibc/blob/master/assert/assert.h).)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This header file reveals another important property of assertions – they can be _turned off_. In C and C++, defining the preprocessor variable `NDEBUG` (\"no debug\") turns off assertions, replacing them with a statement that does nothing. The `NDEBUG` variable can be set during compilation:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -DNDEBUG -g -o testassert testassert.c"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And, as you can see, the assertion has no effect anymore:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testassert"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In Python, assertions can also be turned off, by invoking the `python` interpreter with the `-O` (\"optimize\") flag:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!python -c 'assert 2 + 2 == 5; print(\"Foo\")'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!python -O -c 'assert 2 + 2 == 5; print(\"Foo\")'"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In comparison, which language wins in the amount of assertion diagnostics? Have a look at the information Python provides. If, after defining `fun()` as"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def fun() -> None:\n",
    "    assert 2 + 2 == 5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"If we invoke `fun()` and the assertion fails,\"\n",
    "     \" which information do we get?\",\n",
    "     [\n",
    "         \"The failing condition (`2 + 2 == 5`)\",\n",
    "         \"The location of the assertion in the program\",\n",
    "         \"The list of callers\",\n",
    "         \"All of the above\"\n",
    "     ], '123456789 % 5')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Indeed, a failed assertion (like any exception in Python) provides us with lots of debugging information, even including the source code:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    fun()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Checking Preconditions\n",
    "\n",
    "Assertions show their true power when they are not used in a test, but used in a program instead, because that is when they can check not only _one_ run, but actually _all_ runs."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The classic example for the use of assertions is a _square root_ program, implementing the function $\\sqrt{x}$.  (Let's assume for a moment that the environment does not already have one.) "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We want to ensure that `square_root()` is always called with correct arguments. For this purpose, we set up an assertion:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert x >= 0\n",
    "    ...   # compute square root in y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This assertion is called the _precondition_. A precondition is checked at the beginning of a function.  It checks whether all the conditions for using the function are met.  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "So, if we call `square_root()` with an bad argument, we will get an exception. This holds for _any_ call, ever."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    square_root(-1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For a dynamically typed language like Python, an assertion could actually also check that the argument has the correct type. For `square_root()`, we could ensure that `x` actually has a numeric type:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert isinstance(x, (int, float))\n",
    "    assert x >= 0\n",
    "    ...   # compute square root in y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And while calls with the correct types just work..."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "square_root(4) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "square_root(4.0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "... a call with an illegal type will raise a revealing diagnostic:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    square_root('4')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"If we did not check for the type of `x`, \"\n",
    "     \"would the assertion `x >= 0` still catch a bad call?\",\n",
    "     [\n",
    "         \"Yes, since `>=` is only defined between numbers\",\n",
    "         \"No, because an empty list or string would evaluate to 0\"\n",
    "     ], '0b10 - 0b01')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Fortunately (for us Python users), the assertion `x >= 0` would already catch a number of invalid types, because (in contrast to, say, JavaScript), Python has no implicit conversion of strings or structures to integers:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    '4' >= 0  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Checking Results\n",
    "\n",
    "While a precondition ensures that the _argument_ to a function is correct, a _postcondition_ checks the _result_ of this very function (assuming the precondition held in the first place). For our `square_root()` function, we can check that the result $y = \\sqrt{x}$ is correct by checking that $y^2 = x$ holds:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert x >= 0\n",
    "    ...   # compute square root in y\n",
    "    assert y * y == x"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In practice, we might encounter problems with this assertion. What might these be?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"Why could the assertion fail despite `square_root()` being correct?\",\n",
    "     [\n",
    "         \"We need to compute `y ** 2`, not `y * y`\",\n",
    "         \"We may encounter rounding errors\",\n",
    "         \"The value of `x` may have changed during computation\",\n",
    "         \"The interpreter / compiler may be buggy\"\n",
    "     ], '0b110011 - 0o61')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Technically speaking, there could be many things that _also_ could cause the assertion to fail (cosmic radiation, operating system bugs, secret service bugs, anything) – but the by far most important reason is indeed rounding errors. Here's a simple example, using the Python built-in square root function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import math"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "math.sqrt(2.0) * math.sqrt(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "math.sqrt(2.0) * math.sqrt(2.0) == 2.0"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you want to compare two floating-point values, you need to provide an _epsilon value_ denoting the margin of error."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert x >= 0\n",
    "    ...   # compute square root in y\n",
    "    epsilon = 0.000001\n",
    "    assert abs(y * y - x) < epsilon"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In Python, the function `math.isclose(x, y)` also does the job, by default ensuring that the two values are the same within about 9 decimal digits:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "math.isclose(math.sqrt(2.0) * math.sqrt(2.0), 2.0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "So let's use `math.isclose()` for our revised postcondition:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert x >= 0\n",
    "    ...   # compute square root in y\n",
    "    assert math.isclose(y * y, x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us try out this postcondition by using an actual implementation. The [Newton–Raphson method](https://en.wikipedia.org/wiki/Newton%27s_method) is an efficient way to compute square roots:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def square_root(x):  # type: ignore\n",
    "    assert x >= 0  # precondition\n",
    "\n",
    "    approx = None\n",
    "    guess = x / 2\n",
    "    while approx != guess:\n",
    "        approx = guess\n",
    "        guess = (approx + x / approx) / 2\n",
    "\n",
    "    assert math.isclose(approx * approx, x)\n",
    "    return approx"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Apparently, this implementation does the job:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "square_root(4.0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "However, it is not just this call that produces the correct result – _all_ calls will produce the correct result. (If the postcondition assertion does not fail, that is.) So, a call like"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "square_root(12345.0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "does not require us to _manually_ check the result – the postcondition assertion already has done that for us, and will continue to do so forever."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Assertions and Tests\n",
    "\n",
    "Having assertions right in the code gives us an easy means to _test_ it – if we can feed sufficiently many inputs into the code without the postcondition ever failing, we can increase our confidence. Let us try this out with our `square_root()` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for x in range(1, 10000):\n",
    "    y = square_root(x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Note again that we do not have to check the value of `y` – the `square_root()` postcondition already did that for us."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Instead of enumerating input values, we could also use random (non-negative) numbers; even totally random numbers could work if we filter out those tests where the precondition already fails. If you are interested in such _test generation techniques_, the [Fuzzing Book](fuzzingbook.org) is a great reference for you."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Modern program verification tools even can _prove_ that your program will always meet its assertions. But for all this, you need to have _explicit_ and _formal_ assertions in the first place."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For those interested in testing and verification, here is a quiz for you:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"Is there a value for x that satisfies the precondition, \"\n",
    "    \"but fails the postcondition?\",\n",
    "     [ \n",
    "         \"Yes\",\n",
    "         \"No\"\n",
    "     ], 'int(\"Y\" in \"Yes\")')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is indeed something a test generator or program verifier might be able to find with _zero_ effort."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Partial Checks\n",
    "\n",
    "In the case of `square_root()`, our postcondition is _total_ – if it passes, then the result is correct (within the `epsilon` boundaries, that is). In practice, however, it is not always easy to provide such a total check. As an example, consider our `remove_html_markup()` function from the [Introduction to Debugging](Intro_Debugging.ipynb):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def remove_html_markup(s):  # type: ignore\n",
    "    tag = False\n",
    "    quote = False\n",
    "    out = \"\"\n",
    "\n",
    "    for c in s:\n",
    "        if c == '<' and not quote:\n",
    "            tag = True\n",
    "        elif c == '>' and not quote:\n",
    "            tag = False\n",
    "        elif c == '\"' or c == \"'\" and tag:\n",
    "            quote = not quote\n",
    "        elif not tag:\n",
    "            out = out + c\n",
    "\n",
    "    return out"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "remove_html_markup(\"I am a text with <strong>HTML markup</strong>\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The precondition for `remove_html_markup()` is trivial – it accepts any string. (Strictly speaking, a precondition `assert isinstance(s, str)` could prevent it from being called with some other collection such as a list.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The challenge, however, is the _postcondition_. How do we check that `remove_html_markup()` produces the correct result?\n",
    "\n",
    "* We could check it against some other implementation that removes HTML markup – but if we already do have such a \"golden\" implementation, why bother implementing it again?\n",
    "\n",
    "* After a change, we could also check it against some earlier version to prevent _regression_ – that is, losing functionality that was there before. But how would we know the earlier version was correct? (And if it was, why change it?)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we do not aim for ensuring full correctness, our postcondition can also check for _partial properties_. For instance, a postcondition for `remove_html_markup()` may simply ensure that the result no longer contains any markup:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def remove_html_markup(s):  # type: ignore\n",
    "    tag = False\n",
    "    quote = False\n",
    "    out = \"\"\n",
    "\n",
    "    for c in s:\n",
    "        if c == '<' and not quote:\n",
    "            tag = True\n",
    "        elif c == '>' and not quote:\n",
    "            tag = False\n",
    "        elif c == '\"' or c == \"'\" and tag:\n",
    "            quote = not quote\n",
    "        elif not tag:\n",
    "            out = out + c\n",
    "\n",
    "    # postcondition\n",
    "    assert '<' not in out and '>' not in out\n",
    "\n",
    "    return out"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Besides doing a good job at checking results, the postcondition also does a good job in documenting what `remove_html_markup()` actually does."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"Which of these inputs causes the assertion to fail?\",\n",
    "    [\n",
    "        '`<foo>bar</foo>`',\n",
    "        '`\"foo\"`',\n",
    "        '`>foo<`',\n",
    "        '`\"x > y\"`'\n",
    "    ], '1 + 1 -(-1) + (1 * -1) + 1 ** (1 - 1) + 1')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Indeed. Our (partial) assertion does _not_ detect this error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "remove_html_markup('\"foo\"')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "But it detects this one:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    remove_html_markup('\"x > y\"')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Assertions and Documentation\n",
    "\n",
    "In contrast to \"standard\" documentation such as\n",
    "\n",
    "> `square_root()` expects a non-negative number `x`; its result is $\\sqrt{x}$.\n",
    "\n",
    "assertions have a big advantage: They are _formal_ – and thus have an unambiguous semantics. Notably, we can understand what a function does _uniquely by reading its pre- and postconditions_. Here is an example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def some_obscure_function(x: int, y: int, z: int) -> int:\n",
    "    result = int(...)  # type: ignore\n",
    "    assert x == y == z or result > min(x, y, z)\n",
    "    assert x == y == z or result < max(x, y, z)\n",
    "    return result"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"What does this function do?\",\n",
    "    [\n",
    "        \"It returns the minimum value out of `x`, `y`, `z`\",\n",
    "        \"It returns the middle value out of `x`, `y`, `z`\",\n",
    "        \"It returns the maximum value out of `x`, `y`, `z`\",\n",
    "    ], 'int(0.5 ** math.cos(math.pi))', globals())"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Indeed, this would be a useful (and bug-revealing!) postcondition for one of our showcase functions in the [chapter on statistical debugging](StatisticalDebugger.ipynb)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Using Assertions to Trivially Locate Defects\n",
    "\n",
    "The final benefit of assertions, and possibly even the most important in the context of this book, is _how much assertions help_ with locating defects.\n",
    "Indeed, with proper assertions, it is almost trivial to locate the one function that is responsible for a failure."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider the following situation. Assume I have\n",
    "* a function `f()` whose precondition is satisfied, calling\n",
    "* a function `g()` whose precondition is violated and raises an exception."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "quiz(\"Which function is faulty here?\",\n",
    "     [\n",
    "        \"`g()` because it raises an exception\",\n",
    "        \"`f()`\"\n",
    "        \" because it violates the precondition of `g()`\",\n",
    "        \"Both `f()` and `g()`\"\n",
    "        \" because they are incompatible\",\n",
    "        \"None of the above\"\n",
    "     ], 'math.factorial(int(math.tau / math.pi))', globals())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The rule is very simple: If some function `func()` is called with its preconditions satisfied, and the postcondition of `func()` fail, then the fault in the program state must have originated at some point between these two events. Assuming that all functions called by `func()` also are correct (because their postconditions held), the defect _can only be in the code of `func()`._"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "What pre- and postconditions imply is actually often called a _contract_ between caller and callee:\n",
    "\n",
    "* The caller promises to satisfy the _precondition_ of the callee, \n",
    "whereas\n",
    "* the callee promises to satisfy its own _postcondition_, delivering a correct result.\n",
    "\n",
    "In the above setting, `f()` is the caller, and `g()` is the callee; but as `f()` violates the precondition of `g()`, it has not kept its promises. Hence, `f()` violates the contract and is at fault. `f()` thus  needs to be fixed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Checking Data Structures\n",
    "\n",
    "Let us get back to debugging.  In debugging, assertions serve two purposes: \n",
    "\n",
    "* They immediately detect bugs (if they fail)\n",
    "* They immediately rule out _specific parts of code and state_ (if they pass)\n",
    "\n",
    "This latter part is particularly interesting, as it allows us to focus our search on the lesser checked aspects of code and state. \n",
    "\n",
    "When we say \"code _and_ state\", what do we mean? Actually, assertions can not quickly check several executions of a function, but also _large amounts of data_, detecting faults in data _at the moment they are introduced_."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Times and Time Bombs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us illustrate this by an example.  Let's assume we want a `Time` class that represents the time of day. Its constructor takes the current time using hours, minutes, and seconds. (Note that this is a deliberately simple example – real-world classes for representing time are way more complex.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time:\n",
    "    def __init__(self, hours: int = 0, minutes: int = 0, seconds: int = 0) -> None:\n",
    "        self._hours = hours\n",
    "        self._minutes = minutes\n",
    "        self._seconds = seconds"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To access the individual elements, we introduce a few getters:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def hours(self) -> int:\n",
    "        return self._hours\n",
    "\n",
    "    def minutes(self) -> int:\n",
    "        return self._minutes\n",
    "\n",
    "    def seconds(self) -> int:\n",
    "        return self._seconds"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We allow printing out time, using the [ISO 8601 format](https://en.wikipedia.org/wiki/ISO_8601):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def __repr__(self) -> str:\n",
    "        return f\"{self.hours():02}:{self.minutes():02}:{self.seconds():02}\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Three minutes to midnight can thus be represented as"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "t = Time(23, 57, 0)\n",
    "t"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Unfortunately, there's nothing in our `Time` class that prevents blatant misuse.  We can easily set up a time with negative numbers, for instance:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "t = Time(-1, 0, 0)\n",
    "t"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Such a thing _may_ have some semantics (relative time, maybe?), but it's not exactly conforming to ISO format."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Even worse, we can even _construct_ a `Time` object with strings as numbers."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "t = Time(\"High noon\")  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "and this will be included verbatim the moment we try to print it:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():  # This fails in Python 3.9\n",
    "    print(t)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For now, everything will be fine - but what happens when some other program tries to parse this time? Or processes a log file with a timestamp like this?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In fact, what we have here is a _time bomb_ – a fault in the program state that can sleep for ages until someone steps on it. These are hard to debug, because one has to figure out when the time bomb was set – which can be thousands or millions of lines earlier in the program. Since in the absence of type checking, _any_ assignment to a `Time` object could be the culprit – so good luck with the search."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is again where assertions save the day. What you need is an _assertion that checks whether the data is correct_. For instance, we could revise our constructor such that it checks for correct arguments:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def __init__(self, hours: int = 0, minutes: int = 0, seconds: int = 0) -> None:\n",
    "        assert 0 <= hours <= 23\n",
    "        assert 0 <= minutes <= 59\n",
    "        assert 0 <= seconds <= 60  # Includes leap seconds (ISO8601)\n",
    "\n",
    "        self._hours = hours\n",
    "        self._minutes = minutes\n",
    "        self._seconds = seconds"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "These conditions check whether `hours`, `minutes`, and `seconds` are within the right range. They are called _data invariants_ (or short _invariants_) because they hold for the given data (notably, the internal attributes) at all times.\n",
    "\n",
    "Note the unusual syntax for range checks (this is a Python special), and the fact that seconds can range from 0 to 60.  That's because there's not only leap years, but also leap seconds."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With this revised constructor, we now get errors as soon as we pass an invalid parameter:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    t = Time(-23, 0, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Hence, _any_ attempt to set _any_ Time object to an illegal state will be immediately detected. In other words, the time bomb defuses itself at the moment it is being set."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This means that when we are debugging, and search for potential faults in the state that could have caused the current failure, we can now rule out `Time` as a culprit, allowing us to focus on other parts of the state."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The more of the state we have checked with invariants,\n",
    "\n",
    "* the less state we have to examine, \n",
    "* the fewer possible causes we have to investigate,\n",
    "* the faster we are done with determining the defect."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Invariant Checkers\n",
    "\n",
    "For invariants to be effective, they have to be checked at all times. If we introduce a method that changes the state, then this method will also have to ensure that the invariant is satisfied:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def set_hours(self, hours: int) -> None:\n",
    "        assert 0 <= hours <= 23\n",
    "        self._hours = hours"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This also implies that state changes should go through methods, not direct accesses to attributes. If some code changes the attributes of your object directly, without going through the method that could check for consistency, then it will be much harder for you to a) detect the source of the problem and b) even detect that a problem exists."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Excursion: Checked Getters and Setters in Python"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In Python, the `@property` decorator offers a handy way to implement checkers, even for otherwise direct accesses to attributes. It allows defining specific \"getter\" and \"setter\" functions for individual properties that would even be invoked when a (seemingly) attribute is accessed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Using `@property`, our `Time` class could look like this:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class MyTime(Time):\n",
    "    @property  # type: ignore\n",
    "    def hours(self) -> int:\n",
    "        return self._hours\n",
    "\n",
    "    @hours.setter\n",
    "    def hours(self, new_hours: int) -> None:\n",
    "        assert 0 <= new_hours <= 23\n",
    "        self._hours = new_hours"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To access the current hour, we no longer go through a specific \"getter\" function; instead, we access a synthesized attribute that – behind the scenes – invokes the \"getter\" function marked with `@property`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "my_time = MyTime(11, 30, 0)\n",
    "my_time.hours"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we \"assign\" to the attribute, the \"setter\" function is called in the background;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "my_time.hours = 12  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see this immediately when trying to assign an illegal value:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    my_time.hours = 25  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you build large infrastructures in Python, you can use these features to implement \n",
    "\n",
    "* attributes that are _checked_ every time they are accessed or changed; \n",
    "* attributes that are easier to remember than a large slew of getter and setter functions.\n",
    "\n",
    "In this book, we do not have that many attributes, and we try to use not too many Python-specific features, so we usually go without `@property`. But for Python aficionados, and especially those who care about runtime checks, checked property accesses are a boon."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### End of Excursion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we have several methods that can alter an object, it can be helpful to factor out invariant checking into its own method. Such a method can also be called to check for inconsistencies that might have been introduced without going through one of the methods – e.g. by direct object access, memory manipulation, or memory corruption."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "By convention, methods that check invariants have the name `repOK()`, since they check whether the internal representation is okay, and return True if so."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here's a `repOK()` method for `Time`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def repOK(self) -> bool:\n",
    "        assert 0 <= self.hours() <= 23\n",
    "        assert 0 <= self.minutes() <= 59\n",
    "        assert 0 <= self.seconds() <= 60\n",
    "        return True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can integrate this method right into our constructor and our setter:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def __init__(self, hours: int = 0, minutes: int = 0, seconds: int = 0) -> None:\n",
    "        self._hours = hours\n",
    "        self._minutes = minutes\n",
    "        self._seconds = seconds\n",
    "        assert self.repOK()\n",
    "\n",
    "    def set_hours(self, hours: int) -> None:\n",
    "        self._hours = hours\n",
    "        assert self.repOK()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    t = Time(-23, 0, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Having a single method that checks everything can be beneficial, as it may explicitly check for more faulty states. For instance, it is still permissible to pass a floating-point number for hours and minutes, again breaking the Time representation:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Time(1.5)  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "(Strictly speaking, ISO 8601 _does_ allow fractional parts for seconds and even for hours and minutes – but still wants two leading digits before the fraction separator. Plus, the comma is the \"preferred\" fraction separator. In short, you won't be making too many friends using times formatted like the one above.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can extend our `repOK()` method to check for correct types, too."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def repOK(self) -> bool:\n",
    "        assert isinstance(self.hours(), int)\n",
    "        assert isinstance(self.minutes(), int)\n",
    "        assert isinstance(self.seconds(), int)\n",
    "\n",
    "        assert 0 <= self.hours() <= 23\n",
    "        assert 0 <= self.minutes() <= 59\n",
    "        assert 0 <= self.seconds() <= 60\n",
    "        return True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Time(14, 0, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This now also catches other type errors:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    t = Time(\"After midnight\")  # type: ignore"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Our `repOK()` method can also be used in combination with pre- and postconditions. Typically, you'd like to make it part of the pre- and postcondition checks."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Assume you want to implement an `advance()` method that adds a number of seconds to the current time. The preconditions and postconditions can be easily defined:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Time(Time):\n",
    "    def seconds_since_midnight(self) -> int:\n",
    "        return self.hours() * 3600 + self.minutes() * 60 + self.seconds()\n",
    "\n",
    "    def advance(self, seconds_offset: int) -> None:\n",
    "        old_seconds = self.seconds_since_midnight()\n",
    "\n",
    "        ...  # Advance the clock\n",
    "\n",
    "        assert (self.seconds_since_midnight() ==\n",
    "                (old_seconds + seconds_offset) % (24 * 60 * 60))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "But you'd really like `advance()` to check the state before _and_ after its execution – again using `repOK()`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class BetterTime(Time):\n",
    "    def advance(self, seconds_offset: int) -> None:\n",
    "        assert self.repOK()\n",
    "        old_seconds = self.seconds_since_midnight()\n",
    "\n",
    "        ...  # Advance the clock\n",
    "\n",
    "        assert (self.seconds_since_midnight() ==\n",
    "                (old_seconds + seconds_offset) % (24 * 60 * 60))\n",
    "        assert self.repOK()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The first postcondition ensures that `advance()` produces the desired result; the second one ensures that the internal state is still okay."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Large Data Structures\n",
    "\n",
    "Invariants are especially useful if you have a large, complex data structure which is very hard to track in a conventional debugger."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's assume you have a [red-black search tree](https://en.wikipedia.org/wiki/Red–black_tree) for storing and searching data.  Red-black trees are among the most efficient data structures for representing associative arrays (also known as mappings); they are self-balancing and guarantee search, insertion, and deletion in logarithmic time. They also are among the most ugly to debug."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "What is a red-black tree? Here is an example from Wikipedia:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "![Red-Black Tree](https://upload.wikimedia.org/wikipedia/commons/6/66/Red-black_tree_example.svg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As you can see, there are red nodes and black nodes (giving the tree its name). We can define a class `RedBlackTrees` and implement all the necessary operations."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class RedBlackTree:\n",
    "    RED = 'red'\n",
    "    BLACK = 'black'\n",
    "    ..."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "\n",
    "# A few dummy methods to make the static type checker happy. Ignore.\n",
    "class RedBlackNode:\n",
    "    def __init__(self) -> None:\n",
    "        self.parent = None\n",
    "        self.color = RedBlackTree.BLACK\n",
    "    pass"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "\n",
    "# More dummy methods to make the static type checker happy. Ignore.\n",
    "class RedBlackTree(RedBlackTree):\n",
    "    def redNodesHaveOnlyBlackChildren(self) -> bool:\n",
    "        return True\n",
    "\n",
    "    def equalNumberOfBlackNodesOnSubtrees(self) -> bool:\n",
    "        return True\n",
    "\n",
    "    def treeIsAcyclic(self) -> bool:\n",
    "        return True\n",
    "\n",
    "    def parentsAreConsistent(self) -> bool:\n",
    "        return True\n",
    "\n",
    "    def __init__(self) -> None:\n",
    "        self._root = RedBlackNode()\n",
    "        self._root.parent = None\n",
    "        self._root.color = self.BLACK"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "However, before we start coding, it would be a good idea to _first_ reason about the invariants of a red-black tree. Indeed, a red-black tree has a number of important properties that hold at all times – for instance, that the root node be black or that the tree be balanced. When we implement a red-black tree, these _invariants_ can be encoded into a `repOK()` method:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class RedBlackTree(RedBlackTree):\n",
    "    def repOK(self) -> bool:\n",
    "        assert self.rootHasNoParent()\n",
    "        assert self.rootIsBlack()\n",
    "        assert self.redNodesHaveOnlyBlackChildren()\n",
    "        assert self.equalNumberOfBlackNodesOnSubtrees()\n",
    "        assert self.treeIsAcyclic()\n",
    "        assert self.parentsAreConsistent()\n",
    "        return True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Each of these helper methods are checkers in their own right:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class RedBlackTree(RedBlackTree):\n",
    "    def rootHasNoParent(self) -> bool:\n",
    "        return self._root.parent is None\n",
    "\n",
    "    def rootIsBlack(self) -> bool:\n",
    "        return self._root.color == self.BLACK\n",
    "    ..."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With all these helpers, our `repOK()` method will become very rigorous – but all this rigor is very much needed. Just for fun, check out the [description of red-black trees on Wikipedia](https://en.wikipedia.org/wiki/Red–black_tree). The description of how insertion or deletion work is 4 to 5 pages long (each!), with dozens of special cases that all have to be handled properly. If you ever face the task of implementing such a data structure, be sure to (1) write a `repOK()` method such as the above, and (2) call it before and after each method that alters the tree:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "from typing import Any, List"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class RedBlackTree(RedBlackTree):\n",
    "    def insert(self, item: Any) -> None:\n",
    "        assert self.repOK()\n",
    "        ...  # four pages of code\n",
    "        assert self.repOK()\n",
    "\n",
    "    def delete(self, item: Any) -> None:\n",
    "        assert self.repOK()\n",
    "        ...  # five pages of code\n",
    "        assert self.repOK()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Such checks will make your tree run much slower – essentially, instead of logarithmic time complexity, we now have linear time complexity, as the entire tree is traversed with each change – but you will find any bugs much, much faster. Once your tree goes in production, you can deactivate `repOK()` by default, using some debugging switch to turn it on again should the need ever arise:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class RedBlackTree(RedBlackTree):\n",
    "    def __init__(self, checkRepOK: bool = False) -> None:\n",
    "        ...\n",
    "        self.checkRepOK = checkRepOK\n",
    "\n",
    "    def repOK(self) -> bool:\n",
    "        if not self.checkRepOK:\n",
    "            return True\n",
    "\n",
    "        assert self.rootHasNoParent()\n",
    "        assert self.rootIsBlack()\n",
    "        ...\n",
    "        return True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Just don't delete it – future maintainers of your code will be forever grateful that you have documented your assumptions and given them a means to quickly check their code."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## System Invariants\n",
    "\n",
    "When interacting with the operating system, there are a number of rules that programs must follow, lest they get themselves (or the system) in some state where they cannot execute properly anymore.\n",
    "\n",
    "* If you work with files, every file that you open also must be closed; otherwise, you will deplete resources.\n",
    "* If you create temporary files, be sure to delete them after use; otherwise, you will consume disk space.\n",
    "* If you work with locks, be sure to release locks after use; otherwise, your system may end up in a deadlock.\n",
    "\n",
    "One area in which it is particularly easy to make mistakes is _memory usage_. In Python, memory is maintained by the Python interpreter, and all memory accesses are checked at runtime. Accessing a non-existing element of a string, for instance, will raise a memory error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    index = 10\n",
    "    \"foo\"[index]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The very same expression in a C program, though, will yield _undefined behavior_ – which means that anything can happen. Let us explore a couple of C programs with undefined behavior."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### The C Memory Model\n",
    "\n",
    "We start with a simple C program which uses the same invalid index as our Python expression, above. What does this program do?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "open('testoverflow.c', 'w').write(r'''\n",
    "#include <stdio.h>\n",
    "\n",
    "// Access memory out of bounds\n",
    "int main(int argc, char *argv[]) {\n",
    "    int index = 10;\n",
    "    return \"foo\"[index];  // BOOM\n",
    "}\n",
    "''');"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('testoverflow.c').read())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In our example, the program will read from a random chunk or memory, which may exist or not. In most cases, nothing at all will happen – which is a bad thing, because you won't realize that your program has a defect."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -g -o testoverflow testoverflow.c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testoverflow"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see what is going on behind the scenes, let us have a look at the C memory model."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Excursion: A C Memory Model Simulator"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We build a little simulation of C memory. A `Memory` item stands for a block of continuous memory, which we can access by address using `read()` and `write()`. The `__repr__()` method shows memory contents as a string."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Memory:\n",
    "    def __init__(self, size: int = 10) -> None:\n",
    "        self.size: int = size\n",
    "        self.memory: List[Any] = [None for i in range(size)]\n",
    "\n",
    "    def read(self, address: int) -> Any:\n",
    "        return self.memory[address]\n",
    "\n",
    "    def write(self, address: int, item: Any) -> None:\n",
    "        self.memory[address] = item\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return repr(self.memory)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem: Memory = Memory()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem.write(0, 'a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem.read(0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We introduce `[index]` syntax for easy read and write:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Memory(Memory):\n",
    "    def __getitem__(self, address: int) -> Any:\n",
    "        return self.read(address)\n",
    "\n",
    "    def __setitem__(self, address: int, item: Any) -> None:\n",
    "        self.write(address, item)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem_with_index: Memory = Memory()\n",
    "mem_with_index[1] = 'a'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem_with_index"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem_with_index[1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here are some more advanced methods to show memory cntents. The `repr()` and `_repr_markdown_()` methods display memory as a table. In a notebook, we can simply evaluate the memory to see the table."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from IPython.display import display, Markdown, HTML"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Memory(Memory):\n",
    "    def show_header(self) -> str:\n",
    "        out = \"|Address|\"\n",
    "        for address in range(self.size):\n",
    "            out += f\"{address}|\"\n",
    "        return out + '\\n'\n",
    "\n",
    "    def show_sep(self) -> str:\n",
    "        out = \"|:---|\"\n",
    "        for address in range(self.size):\n",
    "            out += \":---|\"\n",
    "        return out + '\\n'\n",
    "\n",
    "    def show_contents(self) -> str:\n",
    "        out = \"|Content|\"\n",
    "        for address in range(self.size):\n",
    "            contents = self.memory[address]\n",
    "            if contents is not None:\n",
    "                out += f\"{repr(contents)}|\"\n",
    "            else:\n",
    "                out += \" |\"\n",
    "        return out + '\\n'\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return self.show_header() + self.show_sep() + self.show_contents()\n",
    "\n",
    "    def _repr_markdown_(self) -> str:\n",
    "        return repr(self)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem_with_table: Memory = Memory()\n",
    "for i in range(mem_with_table.size):\n",
    "    mem_with_table[i] = 10 * i\n",
    "mem_with_table"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### End of Excursion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In C, memory comes as a single block of bytes at continuous addresses. Let us assume we have a memory of only 20 bytes (duh!) and the string \"foo\" is stored at address 5:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mem_with_table: Memory = Memory(20)\n",
    "mem_with_table[5] = 'f'\n",
    "mem_with_table[6] = 'o'\n",
    "mem_with_table[7] = 'o'\n",
    "mem_with_table"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When we try to access `\"foo\"[10]`, we try to read the memory location at address 15 – which may exist (or not), and which may have arbitrary contents, based on whatever previous instructions left there. From there on, the behavior of our program is undefined."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Such _buffer overflows_ can also come as _writes_ into memory locations – and thus overwrite the item that happens to be at the location of interest. If the item at address 15 happens to be, say, a flag controlling administrator access, then setting it to a non-zero value can come handy for an attacker."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Dynamic Memory\n",
    "\n",
    "A second source of errors in C programs is the use of dynamic memory – that is, memory allocated and deallocated at run-time. In C, the function `malloc()` returns a continuous block of memory of a given size; the function `free()` returns it back to the system.\n",
    "\n",
    "After a block has been `free()`'d, it must no longer be used, as the memory might already be in use by some other function (or program!) again. Here's a piece of code that violates this assumption:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "open('testuseafterfree.c', 'w').write(r'''\n",
    "#include <stdlib.h>\n",
    "\n",
    "// Access a chunk of memory after it has been given back to the system\n",
    "int main(int argc, char *argv[]) {\n",
    "    int *array = malloc(100 * sizeof(int));\n",
    "    free(array);\n",
    "    return array[10];  // BOOM\n",
    "}\n",
    "''');"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('testuseafterfree.c').read())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Again, if we compile and execute this program, nothing tells us that we have just entered undefined behavior:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -g -o testuseafterfree testuseafterfree.c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testuseafterfree"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "What's going on behind the scenes here?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Excursion: Dynamic Memory in C"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`DynamicMemory` introduces dynamic memory allocation `allocate()` and deallocation `free()`, using a list of allocated blocks."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class DynamicMemory(Memory):\n",
    "    # Address at which our list of blocks starts\n",
    "    BLOCK_LIST_START = 0\n",
    "\n",
    "    def __init__(self, *args: Any) -> None:\n",
    "        super().__init__(*args)\n",
    "\n",
    "        # Before each block, we reserve two items:\n",
    "        # One pointing to the next block (-1 = END)\n",
    "        self.memory[self.BLOCK_LIST_START] = -1\n",
    "        # One giving the length of the current block (<0: freed)\n",
    "        self.memory[self.BLOCK_LIST_START + 1] = 0\n",
    "\n",
    "    def allocate(self, block_size: int) -> int:\n",
    "        \"\"\"Allocate a block of memory\"\"\"\n",
    "        # traverse block list \n",
    "        # until we find a free block of appropriate size\n",
    "        chunk = self.BLOCK_LIST_START\n",
    "\n",
    "        while chunk < self.size:\n",
    "            next_chunk = self.memory[chunk]\n",
    "            chunk_length = self.memory[chunk + 1]\n",
    "\n",
    "            if chunk_length < 0 and abs(chunk_length) >= block_size:\n",
    "                # Reuse this free block\n",
    "                self.memory[chunk + 1] = abs(chunk_length)\n",
    "                return chunk + 2\n",
    "\n",
    "            if next_chunk < 0:\n",
    "                # End of list - allocate new block\n",
    "                next_chunk = chunk + block_size + 2\n",
    "                if next_chunk >= self.size:\n",
    "                    break\n",
    "\n",
    "                self.memory[chunk] = next_chunk\n",
    "                self.memory[chunk + 1] = block_size\n",
    "                self.memory[next_chunk] = -1\n",
    "                self.memory[next_chunk + 1] = 0\n",
    "                base = chunk + 2\n",
    "                return base\n",
    "\n",
    "            # Go to next block\n",
    "            chunk = next_chunk\n",
    "\n",
    "        raise MemoryError(\"Out of Memory\")\n",
    "\n",
    "    def free(self, base: int) -> None:\n",
    "        \"\"\"Free a block of memory\"\"\"\n",
    "        # Mark block as available\n",
    "        chunk = base - 2\n",
    "        self.memory[chunk + 1] = -abs(self.memory[chunk + 1])"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In our table, we highlight free blocks in gray:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class DynamicMemory(DynamicMemory):\n",
    "    def show_header(self) -> str:\n",
    "        out = \"|Address|\"\n",
    "        color = \"black\"\n",
    "        chunk = self.BLOCK_LIST_START\n",
    "        allocated = False\n",
    "\n",
    "        # States and colors\n",
    "        for address in range(self.size):\n",
    "            if address == chunk:\n",
    "                color = \"blue\"\n",
    "                next_chunk = self.memory[address]\n",
    "            elif address == chunk + 1:\n",
    "                color = \"blue\"\n",
    "                allocated = self.memory[address] > 0\n",
    "                chunk = next_chunk\n",
    "            elif allocated:\n",
    "                color = \"black\"\n",
    "            else:\n",
    "                color = \"lightgrey\"\n",
    "\n",
    "            item = f'<span style=\"color: {color}\">{address}</span>'\n",
    "            out += f\"{item}|\"\n",
    "        return out + '\\n'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem: DynamicMemory = DynamicMemory(10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem.allocate(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem.allocate(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem.free(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem.allocate(1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    dynamic_mem.allocate(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### End of Excursion"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Dynamic memory is allocated as part of our main memory. The following table shows unallocated memory in gray and allocated memory in black:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem: DynamicMemory = DynamicMemory(13)\n",
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The numbers already stored (-1 and 0) are part of our dynamic memory housekeeping (highlighted in blue); they stand for the next block of memory and the length of the current block, respectively."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us allocate a block of 3 bytes. Our (simulated) allocation mechanism places these at the first continuous block available:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p1 = dynamic_mem.allocate(3)\n",
    "p1"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see that a block of 3 items is allocated at address 2. The two numbers before that address (5 and 3) indicate the beginning of the next block as well as the length of the current one."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us allocate some more."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p2 = dynamic_mem.allocate(4)\n",
    "p2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can make use of that memory:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem[p1] = 123\n",
    "dynamic_mem[p2] = 'x'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When we free memory, the block is marked as free by giving it a negative length:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem.free(p1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Note that freeing memory does not clear memory; the item at `p1` is still there. And we can also still access it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem[p1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "But if, in the meantime, some other part of the program requests more memory and uses it..."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p3 = dynamic_mem.allocate(2)\n",
    "dynamic_mem[p3] = 'y'\n",
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "... then the memory at `p1` may simply be overwritten."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem[p1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "An even worse effect comes into play if one accidentally overwrites the dynamic memory allocation information; this can easily corrupt the entire memory management. In our case, such corrupted memory can lead to an endless loop when trying to allocate more memory:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ExpectError import ExpectTimeout"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem[p3 + 3] = 0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "dynamic_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When `allocate()` traverses the list of blocks, it will enter an endless loop between the block starting at address 0 (pointing to the next block at 5) and the block at address 5 (pointing back to 0)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectTimeout(1):\n",
    "    dynamic_mem.allocate(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Real-world `malloc()` and `free()` implementations suffer from similar problems. As stated above: As soon as undefined behavior is reached, anything may happen."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Managed Memory\n",
    "\n",
    "The solution to all these problems is to _keep track of memory_, specifically\n",
    "\n",
    "* which parts of memory have been _allocated_, and\n",
    "* which parts of memory have been _initialized_."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To this end, we introduce two extra flags for each address:\n",
    "\n",
    "* The `allocated` flag tells whether an address has been allocated; the `allocate()` method sets them, and `free()` clears them again.\n",
    "* The `initialized` flag tells whether an address has been written to. This is cleared as part of `allocate()`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With these, we can run a number of checks:\n",
    "\n",
    "* When _writing_ into memory and _freeing_ memory, we can check whether the address has been _allocated_; and\n",
    "* When _reading_ from memory, we can check whether the address has been allocated and _initialized_.\n",
    "\n",
    "Both of these should effectively prevent memory errors."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Excursion: Managed Memory"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We create a simulation of managed memory. `ManagedMemory` keeps track of every address whether it is initialized and allocated."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class ManagedMemory(DynamicMemory):\n",
    "    def __init__(self, *args: Any) -> None:\n",
    "        super().__init__(*args)\n",
    "        self.initialized = [False for i in range(self.size)]\n",
    "        self.allocated = [False for i in range(self.size)]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This allows memory access functions to run a number of extra checks:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class ManagedMemory(ManagedMemory):\n",
    "    def write(self, address: int, item: Any) -> None:\n",
    "        assert self.allocated[address], \\\n",
    "            \"Writing into unallocated memory\"\n",
    "        self.memory[address] = item\n",
    "        self.initialized[address] = True\n",
    "\n",
    "    def read(self, address: int) -> Any:\n",
    "        assert self.allocated[address], \\\n",
    "            \"Reading from unallocated memory\"\n",
    "        assert self.initialized[address], \\\n",
    "            \"Reading from uninitialized memory\"\n",
    "        return self.memory[address]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Dynamic memory functions are set up such that they keep track of these flags."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class ManagedMemory(ManagedMemory):\n",
    "    def allocate(self, block_size: int) -> int:\n",
    "        base = super().allocate(block_size)\n",
    "        for i in range(block_size):\n",
    "            self.allocated[base + i] = True\n",
    "            self.initialized[base + i] = False\n",
    "        return base\n",
    "\n",
    "    def free(self, base: int) -> None:\n",
    "        assert self.allocated[base], \\\n",
    "            \"Freeing memory that is already freed\"\n",
    "        block_size = self.memory[base - 1]\n",
    "        for i in range(block_size):\n",
    "            self.allocated[base + i] = False\n",
    "            self.initialized[base + i] = False\n",
    "        super().free(base)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us highlight these flags when printing out the table:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class ManagedMemory(ManagedMemory):\n",
    "    def show_contents(self) -> str:\n",
    "        return (self.show_allocated() + \n",
    "               self.show_initialized() +\n",
    "            DynamicMemory.show_contents(self))\n",
    "\n",
    "    def show_allocated(self) -> str:\n",
    "        out = \"|Allocated|\"\n",
    "        for address in range(self.size):\n",
    "            if self.allocated[address]:\n",
    "                out += \"Y|\"\n",
    "            else:\n",
    "                out += \" |\"\n",
    "        return out + '\\n'\n",
    "\n",
    "    def show_initialized(self) -> str:\n",
    "        out = \"|Initialized|\"\n",
    "        for address in range(self.size):\n",
    "            if self.initialized[address]:\n",
    "                out += \"Y|\"\n",
    "            else:\n",
    "                out += \" |\"\n",
    "        return out + '\\n'"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### End of Excursion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here comes a simple simulation of managed memory. After we create memory, all addresses are neither allocated nor initialized:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "managed_mem: ManagedMemory = ManagedMemory()\n",
    "managed_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us allocate some elements. We see that the first three bytes are now marked as allocated:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p = managed_mem.allocate(3)\n",
    "managed_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "After writing into memory, the respective addresses are marked as \"initialized\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "managed_mem[p] = 10\n",
    "managed_mem[p + 1] = 20"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "managed_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Attempting to read uninitialized memory fails:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    x = managed_mem[p + 2]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When we free the block again, it is marked as not allocated:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "managed_mem.free(p)\n",
    "managed_mem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And accessing any element of the free'd block will yield an error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    managed_mem[p] = 10"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Freeing the same block twice also yields an error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    managed_mem.free(p)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With this, we now have a mechanism in place to fully detect memory issues in languages such as C."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Obviously, keeping track of whether memory is allocated/initialized or not requires some extra memory – and also some extra computation time, as read and write accesses have to be checked first. During testing, however, such effort may quickly pay off, as memory bugs can be quickly discovered."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To detect memory errors, a number of tools have been developed. The first class of tools _interprets_ the instructions of the executable code, tracking all memory accesses. For each memory access, they can check whether the memory accessed _exists_ and has been _initialized_ at some point."
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Checking Memory Usage with Valgrind\n",
    "\n",
    "The [Valgrind](https://www.valgrind.org) tool allows _interpreting_ executable code, thus tracking each and every memory access. You can use Valgrind to execute any program from the command-line, and it will check all memory accesses during execution. \n",
    "\n",
    "<!-- Installing ValGrind on macOS: https://github.com/LouisBrunner/valgrind-macos/ -->\n",
    "\n",
    "Here's what happens if we run Valgrind on our `testuseafterfree` program:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('testuseafterfree.c').read())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!valgrind ./testuseafterfree"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see that Valgrind has detected the issue (\"Invalid read of size 4\") during execution; it also reported the current stack trace (and hence the location at which the error occurred). Note that the program continues execution even after the error occurred; should further errors occur, Valgrind will report these, too."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Being an interpreter, Valgrind slows down execution of programs dramatically. However, it requires no recompilation and thus can work on code (and libraries) whose source code is not available."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Valgrind is not perfect, though. For our `testoverflow` program, it fails to detect the illegal access:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print_content(open('testoverflow.c').read())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!valgrind ./testoverflow"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is because at compile time, the information about the length of the `\"foo\"` string is no longer available – all Valgrind sees is a read access into the static data portion of the executable that may be valid or invalid. To actually detect such errors, we need to hook into the compiler."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Checking Memory Usage with Memory Sanitizer\n",
    "\n",
    "The second class of tools to detect memory issues are _address sanitizers_. An address sanitizer injects memory-checking code into the program _during compilation_. This means that every access will be checked – but this time, the code still runs on the processor itself, meaning that the speed is much less reduced."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here is an example of how to use the address sanitizer of the Clang C compiler:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -fsanitize=address -o testuseafterfree testuseafterfree.c"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "At the very first moment we have an out-of-bounds access, the program aborts with a diagnostic message – in our case already during `read_overflow()`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testuseafterfree"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Likewise, if we apply the address sanitizer on `testoverflow`, we also immediately get an error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cc -fsanitize=address -o testoverflow testoverflow.c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!./testoverflow"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Since the address sanitizer monitors each and every read and write, as well as usage of `free()`, it will require some effort to create a bug that it won't catch. Also, while Valgrind runs the program ten times slower and more, the performance penalty for memory sanitization is much much lower. Sanitizers can also help in finding data races, memory leaks, and all other sorts of undefined behavior. As [Daniel Lemire puts it](https://lemire.me/blog/2016/04/20/no-more-leaks-with-sanitize-flags-in-gcc-and-clang/):\n",
    "\n",
    "> Really, if you are using gcc or clang and you are not using these flags, you are not being serious."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## When Should Invariants be Checked?\n",
    "\n",
    "We have seen that during testing and debugging, invariants should be checked _as much as possible_, thus narrowing down the time it takes to detect a violation to a minimum. The easiest way to get there is to have them checked as _postcondition_ in the constructor and any other method that sets the state of an object."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you have means to alter the state of an object outside of these methods – for instance, by directly writing to memory, or by writing to internal attributes –, then you may have to check them even more frequently. Using the [tracing infrastructure](Tracer.ipynb), for instance, you can have the tracer invoke `repOK()` with each and every line executed, thereby again directly pinpointing the moment the state gets corrupted. While this will slow down execution tremendously, it is still better to have the computer do the work than you stepping backwards and forwards through an execution."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another question is whether assertions should remain active even in production code. Assertions take time, and this may be too much for production."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Assertions are not Production Code\n",
    "\n",
    "First of all, assertions are _not_ production code – the rest of the code should not be impacted by any assertion being on or off. If you write code like\n",
    "\n",
    "```python\n",
    "assert map.remove(location)\n",
    "```\n",
    "your assertion will have a side effect, namely removing a location from the map.  If one turns assertions off, the side effect will be turned off as well.  You need to change this into\n",
    "\n",
    "```python\n",
    "locationRemoved = map.remove(location)\n",
    "assert locationRemoved\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### For System Preconditions, Use Production Code \n",
    "\n",
    "Consequently, you should not rely on assertions for _system preconditions_  – that is, conditions that are necessary to keep the system running. System input (or anything that could be controlled by another party) still has to be validated by production code, not assertions. Critical conditions have to be checked by production code, not (only) assertions.\n",
    "\n",
    "If you have code such as\n",
    "```python\n",
    "assert command in {\"open\", \"close\", \"exit\"}\n",
    "exec(command)\n",
    "```\n",
    "then having the assertion document and check your assumptions is fine. However, if you turn the assertion off in production code, it will only be a matter of time until somebody sets `command` to `'system(\"/bin/sh\")'` and all of a sudden takes control over your system."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Consider Leaving Some Assertions On\n",
    "\n",
    "The main reason for turning assertions off is efficiency. However, _failing early is better than having bad data and not failing._ Think carefully which assertions have a high impact on execution time, and turn these off first. Assertions that have little to no impact on resources can be left on."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As an example, here's a piece of code that handles traffic in a simulation. The `light` variable can be either `RED`, `AMBER`, or `GREEN`:\n",
    "\n",
    "```python\n",
    "if light == RED:\n",
    "   traffic.stop()\n",
    "elif light == AMBER:\n",
    "   traffic.prepare_to_stop()\n",
    "elif light == GREEN:\n",
    "   traffic.go()\n",
    "else:\n",
    "   pass   # This can't happen!\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Having an assertion\n",
    "\n",
    "```python\n",
    "assert light in [RED, AMBER, GREEN]\n",
    "```\n",
    "\n",
    "in your code will eat some (minor) resources. However, adding a line\n",
    "\n",
    "```python\n",
    "assert False\n",
    "```\n",
    "\n",
    "in the place of the `This can't happen!` line, above, will still catch errors, but require no resources at all."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you have very critical software, it may be wise to actually pay the extra penalty for assertions (notably system assertions) rather than sacrifice reliability for performance. Keeping a memory sanitizer on even in production can have a small impact on performance, but will catch plenty of errors before some corrupted data (and even some attacks) have bad effects downstream."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Define How Your Application Should Handle Internal Errors\n",
    "\n",
    "By default, failing assertions are not exactly user-friendly – the diagnosis they provide is of interest to the code maintainers only.  Think of how your application should handle internal errors as discovered by assertions (or the runtime system). Simply exiting (as assertions on C do) may not be the best option for critical software. Think about implementing your own assert functions with appropriate recovery methods."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Synopsis"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This chapter discusses _assertions_ to define _assumptions_ on function inputs and results:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def my_square_root(x):  # type: ignore\n",
    "    assert x >= 0\n",
    "    y = square_root(x)\n",
    "    assert math.isclose(y * y, x)\n",
    "    return y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Notably, assertions detect _violations_ of these assumptions at runtime:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    y = my_square_root(-1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "_System assertions_ help to detect invalid memory operations."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "managed_mem = ManagedMemory()\n",
    "managed_mem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with ExpectError():\n",
    "    x = managed_mem[2]"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Lessons Learned\n",
    "\n",
    "* _Assertions_ are powerful tools to have the computer check invariants during execution:\n",
    "    * _Preconditions_ check whether the arguments to a function are correct\n",
    "    * _Postconditions_ check whether the result of a function is correct\n",
    "    * _Data Invariants_ allow checking data structures for integrity\n",
    "* Since assertions can be turned off for optimization, they should\n",
    "    * not _change correct operation_ in any way\n",
    "    * not do _any work that your application requires for correct operation_\n",
    "    * not be used as a _replacement for errors that can possibly happen_; create permanent checks (and own exceptions) for these\n",
    "* _System assertions_ are powerful tools to monitor the integrity of the runtime system (notably memory)\n",
    "* The more assertions,\n",
    "    * the earlier errors are detected\n",
    "    * the easier it is to locate defects\n",
    "    * the better the guidance towards failure causes during debugging"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "import os\n",
    "import shutil"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "# Let's cleanup things\n",
    "for path in [\n",
    "                'assert.h',\n",
    "                'testassert',\n",
    "                'testassert.c',\n",
    "                'testassert.dSYM',\n",
    "                'testoverflow',\n",
    "                'testoverflow.c',\n",
    "                'testoverflow.dSYM',\n",
    "                'testuseafterfree',\n",
    "                'testuseafterfree.c',\n",
    "                'testuseafterfree.dSYM',\n",
    "            ]:\n",
    "    if os.path.isdir(path):\n",
    "        shutil.rmtree(path)\n",
    "    else:\n",
    "        try:\n",
    "            os.remove(path)\n",
    "        except FileNotFoundError:\n",
    "            pass"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": false,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Next Steps\n",
    "\n",
    "In the next chapters, we will learn how to\n",
    "\n",
    "* [identify performance issues](PerformanceDebugger.ipynb)\n",
    "* [check flows and dependencies](Slicer.ipynb)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Background\n",
    "\n",
    "The usage of _assertions_ goes back to the earliest days of programming. In 1947, Neumann and Goldstine defined _assertion boxes_ that would check the limits of specific variables. In his 1949 talk [\"Checking a Large Routine\"](http://www.turingarchive.org/browse.php/B/8), Alan Turing suggested\n",
    "\n",
    "> How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, the programmer should make a number of definite _assertions_ which can be checked individually, and from which the correctness of the whole program easily follows.\n",
    "\n",
    "[Valgrind](https://valgrind.org) originated as an academic tool which has seen lots of industrial usage. A [list of papers](https://www.valgrind.org/docs/pubs.html) is available on the Valgrind page.\n",
    "\n",
    "The [Address Sanitizer](http://clang.llvm.org/docs/AddressSanitizer.html) discussed in this chapter was developed at Google; the [paper by Serebryany](https://www.usenix.org/system/files/conference/atc12/atc12-final39.pdf) discusses several details."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "## Exercises"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "button": false,
    "new_sheet": true,
    "run_control": {
     "read_only": false
    }
   },
   "source": [
    "### Exercise 1 – Storage Assertions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The Python [`shelve`](https://docs.python.org/3/library/shelve.html) module provides a simple interface for permanent storage of Python objects:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import shelve"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d = shelve.open('mydb')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d['123'] = 123"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d['123']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d.close()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d = shelve.open('mydb')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d['123']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "d.close()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Based on `shelve`, we can implement a class `ObjectStorage` that uses a context manager (a `with` block) to ensure the shelve database is always closed - also in presence of exceptions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# ignore\n",
    "from typing import Sequence, Any, Callable, Optional, Type, Tuple, Any\n",
    "from typing import Dict, Union, Set, List, FrozenSet, cast"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from types import TracebackType"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Storage:\n",
    "    def __init__(self, dbname: str) -> None:\n",
    "        self.dbname = dbname\n",
    "\n",
    "    def __enter__(self) -> Any:\n",
    "        self.db = shelve.open(self.dbname)\n",
    "        return self\n",
    "\n",
    "    def __exit__(self, exc_tp: Type, exc_value: BaseException, \n",
    "                 exc_traceback: TracebackType) -> Optional[bool]:\n",
    "        self.db.close()\n",
    "        return None\n",
    "\n",
    "    def __getitem__(self, key: str) -> Any:\n",
    "        return self.db[key]\n",
    "\n",
    "    def __setitem__(self, key: str, value: Any) -> None:\n",
    "        self.db[key] = value"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "with Storage('mydb') as storage:\n",
    "    print(storage['123'])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "source": [
    "#### Task 1 – Local Consistency\n",
    "\n",
    "Extend `Storage` with assertions that ensure that after adding an element, it also can be retrieved with the same value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "source": [
    "**Solution.** One single assertion suffices:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "class Storage(Storage):\n",
    "    def __setitem__(self, key: str, value: Any) -> None:\n",
    "        self.db[key] = value\n",
    "        assert self.db[key] == value"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "source": [
    "#### Task 2 – Global Consistency\n",
    "\n",
    "Extend `Storage` with a \"shadow dictionary\" which holds elements in memory storage, too. Have a `repOK()` method that memory storage and `shelve` storage are identical at all times."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "source": [
    "**Solution.** Here is a possible implementation:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "class ShadowStorage:\n",
    "    def __init__(self, dbname: str) -> None:\n",
    "        self.dbname = dbname\n",
    "\n",
    "    def __enter__(self) -> Any:\n",
    "        self.db = shelve.open(self.dbname)\n",
    "        self.memdb = {}\n",
    "        for key in self.db.keys():\n",
    "            self.memdb[key] = self.db[key]\n",
    "        assert self.repOK()\n",
    "        return self\n",
    "\n",
    "    def __exit__(self, exc_tp: Type, exc_value: BaseException, \n",
    "                 exc_traceback: TracebackType) -> Optional[bool]:\n",
    "        self.db.close()\n",
    "        return None\n",
    "\n",
    "    def __getitem__(self, key: str) -> Any:\n",
    "        assert self.repOK()\n",
    "        return self.db[key]\n",
    "\n",
    "    def __setitem__(self, key: str, value: Any) -> None:\n",
    "        assert self.repOK()\n",
    "        self.memdb[key] = self.db[key] = value\n",
    "        assert self.repOK()\n",
    "\n",
    "    def repOK(self) -> bool:\n",
    "        assert self.db.keys() == self.memdb.keys(), f\"{self.dbname}: Differing keys\"\n",
    "        for key in self.memdb.keys():\n",
    "            assert self.db[key] == self.memdb[key], \\\n",
    "                f\"{self.dbname}: Differing values for {repr(key)}\"\n",
    "        return True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "with ShadowStorage('mydb') as storage:\n",
    "    storage['456'] = 456\n",
    "    print(storage['123'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "# ignore\n",
    "try:\n",
    "    os.remove('mydb.db')  # on macOS\n",
    "except FileNotFoundError:\n",
    "    pass"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "skip"
    },
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "# ignore\n",
    "try:\n",
    "    os.remove('mydb')  # on Linux\n",
    "except FileNotFoundError:\n",
    "    pass"
   ]
  }
 ],
 "metadata": {
  "ipub": {
   "bibliography": "fuzzingbook.bib",
   "toc": true
  },
  "kernelspec": {
   "display_name": "venv",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.10 (main, Jan 15 2022, 11:48:04) \n[Clang 13.0.0 (clang-1300.0.29.3)]"
  },
  "toc": {
   "base_numbering": 1,
   "nav_menu": {},
   "number_sections": true,
   "sideBar": true,
   "skip_h1_title": true,
   "title_cell": "",
   "title_sidebar": "Contents",
   "toc_cell": false,
   "toc_position": {},
   "toc_section_display": true,
   "toc_window_display": true
  },
  "toc-autonumbering": false,
  "toc-showmarkdowntxt": false,
  "vscode": {
   "interpreter": {
    "hash": "0af4f07dd039d1b4e562c7a7d0340393b1c66f50605ac6af30beb81aa23b7ef5"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}