lect5.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Лекция №5. Автоматизация тестирования\n",
    "\n",
    "П.Н. Советов, РТУ МИРЭА"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Программные ошибки и верификация\n",
    "\n",
    "В процессе обучения программированию типична ситуация, когда ученик свою программу, которая \"вроде бы работает\", отдает на проверку преподавателю. Преподаватель оценивает выполнение требований, заданных в условии задачи и выявляет возможные ошибки.\n",
    "\n",
    "В общем же, недостаточно написать программу, которая \"вроде бы работает\". Программист должен иметь уверенность в том, что cозданная программа соответствует требованиям и в ней нет серьезных ошибок. Это особенно важно, когда речь идет не об ученике, который полагается на мнение преподавателя, а о профессиональном разработчике ПО.\n",
    "\n",
    "Насколько опасными могут быть программные ошибки? В литературе часто приводятся следующие классические примеры:\n",
    "\n",
    "* Середина 80-х годов, ошибки в ПО медицинского аппарата для лучевой терапии \"Therac-25\" привели к смерти как минимум двух пациентов.\n",
    "* 1991 год, Ирак, ЗРК \"Пэтриот\" из-за программной ошибки, связанной с потерей точности вычислений, не сумел перехватить советскую ракету Р-17, в результате чего погибло 28 американских солдат.\n",
    "* 1994 год, ошибка в реализации команды деления процессора Pentium компании Intel привела к значительным затратам на бесплатную замену микросхем.\n",
    "* 1996 год, из-за ошибки преобразования данных в бортовом ПО взорвалась европейская ракета-носитель \"Ариан 5\".\n",
    "\n",
    "Можно вспомнить и более современные случаи последствий программных ошибок: крушение Боинга 737 MAX 8, приостановка работы марсохода Curiosity и многие другие [примеры](https://www5.in.tum.de/~huckle/bugse.html).\n",
    "\n",
    "Что считать ошибкой в программе? Понятно, что недопустимыми являются ситуации, когда программа \"зависает\" или \"падает\" с выводом сообщения от интерпретатора. Важнейшим классом ошибок являются ошибки несоответствия решения заданным требованиям, то есть спецификации:\n",
    "\n",
    "> \"Без спецификации нет ошибок — есть только сюрпризы\" (Б. Керниган)\n",
    "\n",
    "Спецификация может быть задана неформальным образом, в виде некоторого документа на естественном языке. Менее популярным на практике, но имеющим большие перспективы является использование формальной спецификации, когда требования к ПО описываются в строгой форме, с помощью некоторого математического формализма.\n",
    "\n",
    "В спецификации различают функциональные и нефункциональные требования. К последним относят такие требования, как производительность системы, ее безопасность и эргономика.\n",
    "\n",
    "Проверка соответствия программы предъявляемым ей требованиям, то есть спецификации, называется верификацией."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Формальная верификация\n",
    "\n",
    "Верификацию программной системы легче проводить, абстрагируясь, отвлекаясь от несущественных для анализа деталей. При этом проверке на отсутствие ошибок подвергается не сама система, а ее модель.\n",
    "\n",
    "Заслуживающим внимания является подход модельно-ориентированного проектирования (Model-driven development). В этом подходе строго формулируется модель системы, построенная по спецификации. Существуют специализированные инструменты, такие, как [Simulink](https://www.mathworks.com/help/simulink/gs/model-based-design.html), которые позволяют оценить характеристики высокоуровневой исполняемой модели, а также автоматически получить из модели реализацию, то есть программный код.\n",
    "\n",
    "При использовании методов формальной верификации программная система и ее спецификация описываются математическими моделями и далее осуществляется строгое доказательство того, что система работает корректно. Специалист в области формальной верификации должен обладать специфическими знаниями и навыками, далекими от того, что умеет обычный разработчик. Сами методы формальной верификации плохо масштабируются: обычно удается доказать корректность только для сравнительно небольших программ. В этой связи рассматриваемые методы применяются только в самых ответственных областях: бортовом ПО, медицинской аппаратуре, ядрах ОС и так далее.\n",
    "\n",
    "Важно помнить, что при использовании формальных методов речь, фактически, идет о доказательстве корректности для идеализированного описания системы, а не самой системы. Здесь можно вспомнить известную фразу Д. Кнута:\n",
    "\n",
    "> \"Остерегайтесь ошибок в вышеуказанном коде, я только доказал его правильность, но не пробовал выполнить его\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Тестирование\n",
    "\n",
    "Еще одним способом верификации ПО являются методы тестирования, которые проверяют поведение реализации программной системы на некотором наборе тестовых сценариев. Задача тестирования значительно скромнее задачи формальной верификации:\n",
    "\n",
    "> \"Тестирование программ можно использовать для того, чтобы показать наличие ошибок и никогда — для того чтобы показать их отсутствие!\" (Э. Дейкстра)\n",
    "\n",
    "Тестирование может быть произведено вручную, но значительно более продуктивно использовать методы автоматизации тестирования, которые подразумевают создание специальных тестирующих программ. \n",
    "\n",
    "Тестирование может производиться в различных масштабах:\n",
    "\n",
    "1. Модульные тесты (unit tests). Тесты отдельных функцией, классов или модулей. К модульным относят также регрессионные тесты (проверка на появление уже исправленных ранее ошибок после очередной модификации кода) и макетные тесты (замена реальных входов и выходов тестируемого модуля макетами).\n",
    "1. Интеграционные тесты. Тесты на интеграцию модулей. Недостаточно проверить каждый модуль отдельно, новое поведение возникает, когда эти модули друг с другом взаимодействуют.\n",
    "1. Системные (приемочные) тесты. Тестирование всей программной системы с использованием входов и выходов, доступных пользователю этой системы.\n",
    "\n",
    "Различают тестирование черного и белого ящиков:\n",
    "\n",
    "1. В тестировании черного ящика при порождения тестовых сценариев используется только информация о спецификации системы.\n",
    "1. В случае тестирования белого ящика для организации тестов и оценки качества тестирования анализируется внутренняя структура программы.\n",
    "\n",
    "С точки зрения вопросов организации тестовых сценариев программные системы можно разделить на следующие классы:\n",
    "\n",
    "1. Трансформирующая система. Это система, не имеющая состояния и осуществляющая однократное преобразование входных данных в выходные. Тестовым сценарием здесь будет пара, состоящая из примера входных и выходных данных.\n",
    "2. Реактивная (реагирующая) система. Это система, взаимодействующая с внешней средой путем обмена сообщениями в темпе, задаваемом средой. В таких системах имеется состояние, то есть поведение зависит не только от входных данных, но и от истории предыдущих обменов сообщениями. Тестовым сценарием здесь является последовательность (или даже граф — в случае наличия недетерминизма в работе системы) входных и выходных сообщений. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Разработка с учетом тестирования\n",
    "\n",
    "Упростить тестирование (и в целом верификацию) программной системы можно, используя известные приемы проектирования ПО:\n",
    "\n",
    "1. Разбить систему на набор независимых модулей, каждый из которых выполняет только одну функцию.\n",
    "1. Уменьшить число связей между взаимодействующими модулями.\n",
    "1. Четко разделить интерфейсную и вычислительную части системы.\n",
    "\n",
    "Универсальным средством является написание краткого, простого, легко читаемого кода:\n",
    "\n",
    "> \"Есть два способа разработки проекта приложения: сделать его настолько простым, чтобы было очевидно, что в нем нет\n",
    "недостатков, или сделать его таким сложным, чтобы в нем не было очевидных недостатков\" (Ч. Хоар)\n",
    "\n",
    "Подход разработки через тестирование (TDD, Test-driven development) предполагает написание тестов еще до реализации проверяемого свойства системы. Основные шаги итерационного процесса TDD включают в себя:\n",
    "\n",
    "1. Написание модульных тестов, отражающих требования к очередному программному компоненту.\n",
    "1. Запуск тестов, с ожиданием неуспеха, поскольку требования еще не были реализованы в программном коде.\n",
    "1. Написание кода программного компонента в достаточной степении для успешного прохождения тестов.\n",
    "\n",
    "При использовании TDD упрощаются модификации программного кода (рефакторинг), поскольку для проверки корректности очередных изменений можно использовать заранее реализованные тесты.\n",
    "\n",
    "Важно отметить, что затраты на тестирование не должны превышать затраты на само конструирование программной системы. В противном случае тестирование, скорее всего, окажется слишком дорогостоящим для большинства проектов. Впрочем, если возвратиться к методам формальной верификации, то там значительно (иной раз, на несколько порядков!) более высокая сложность доказательства корректности ПО, чем построение самого ПО, оправдана, поскольку позволяет сохранить жизни людей и избежать затрат на устранение последствий катастроф."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Оператор assert\n",
    "\n",
    "Этот оператор используется для вставки отладочных утверждений в код и, зачастую, оказывается предпочтительнее привычной многим программистам отладочной печати:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Реализация факториала с ошибкой\n",
    "def wrong_fact(n):\n",
    "    assert n >= 0, f'ошибочный аргумент {n}'\n",
    "    return n * wrong_fact(n - 1)\n",
    "\n",
    "# Раскомментируйте, чтобы получить исключение AssertionError\n",
    "# wrong_fact(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Оператор assert имеет следующий вид:\n",
    "\n",
    "```Python\n",
    "assert утверждение\n",
    "```\n",
    "\n",
    "или\n",
    "\n",
    "```Python\n",
    "assert утверждение, выражение\n",
    "```\n",
    "\n",
    "Здесь утверждение возвращает булево значение. Если утверждение истинно, то выполнение программы продолжится, в противном случае будет вызвано исключение AssertionError. Выражение может быть добавлено через запятую к утверждению, чтобы указать дополнительную информацию (в нашем случае это значение аргумента wrong_fact) при вызове исключения.\n",
    "\n",
    "Оператор assert используется во многих системах тестирования, реализованных на Питоне."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Тестирование вместе с документированием"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Модуль doctest совмещает в себе функции легковесного документирования и тестирования. Строка docstring в теле функции анализируется на предмет фрагментов REPL-диалога с интерпретатором и получаемые результаты сравниваются с ожидаемыми:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "def fact(n):\n",
    "    '''\n",
    "    Реализация вычисления факториала.\n",
    "    >>> fact(5)\n",
    "    120\n",
    "    >>> fact(0)\n",
    "    1\n",
    "    >>> fact(-1)\n",
    "    Traceback (most recent call last):\n",
    "        ...\n",
    "    RecursionError: maximum recursion depth exceeded in comparison\n",
    "    '''\n",
    "    if n in range(0, 1):\n",
    "        return 1       \n",
    "    return n * fact(n - 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "В примере выше используется три тестовых сценария. В случае f(-1) излишняя информация о возникшем исключении пропускается с помощью `...`. Запустить тесты можно с помощью командной строки:\n",
    "\n",
    "```\n",
    "python -m doctest -v fact.py\n",
    "```\n",
    "\n",
    "Будет получен следующий результат:\n",
    "\n",
    "```\n",
    "Trying:\n",
    "    fact(5)\n",
    "Expecting:\n",
    "    120\n",
    "ok\n",
    "Trying:\n",
    "    fact(0)\n",
    "Expecting:\n",
    "    1\n",
    "ok\n",
    "Trying:\n",
    "    fact(-1)\n",
    "Expecting:\n",
    "    Traceback (most recent call last):\n",
    "        ...\n",
    "    RecursionError: maximum recursion depth exceeded in comparison\n",
    "ok\n",
    "1 items had no tests:\n",
    "    fact\n",
    "1 items passed all tests:\n",
    "   3 tests in fact.fact\n",
    "3 tests in 2 items.\n",
    "3 passed and 0 failed.\n",
    "Test passed.\n",
    "```\n",
    "\n",
    "При необходимости тесты можно вынести в отдельный файл, с расширением, отличным от '.py'. Это может быть файл с документацией по проекту в форматах `.rst` или `.md`. В нашем примере может использоваться отдельный файл fact.doctest:\n",
    "\n",
    "```\n",
    "# Документация\n",
    "\n",
    "Пример вычисления факториала.\n",
    "\n",
    ">>> from fact import fact\n",
    ">>> fact(5)\n",
    "120\n",
    "```\n",
    "\n",
    "```\n",
    "python -m doctest fact.doctest \n",
    "```\n",
    "\n",
    "При вызове модуля doctest без ключа `-v` сообщение будет выдано только если при прогоне тестов была обнаружена ошибка.\n",
    "\n",
    "Остается добавить, что существуют генераторы документации, которые автоматически извлекают docstring-фрагменты из исходного кода и формируют результат в виде справочного руководства по функциям программного проекта."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Универсальный фреймворк для задач тестирования\n",
    "\n",
    "Модуль [pytest](https://docs.pytest.org/en/stable/contents.html) является сторонним и требует установки:\n",
    "\n",
    "```\n",
    "pip install pytest\n",
    "```\n",
    "\n",
    "Предыдущий пример с факториалом в случае pytest будет выглядеть так:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pytest\n",
    "\n",
    "\n",
    "def test_fact():\n",
    "    assert fact(5) == 120\n",
    "    assert fact(0) == 1\n",
    "    with pytest.raises(RecursionError): # Ожидается исключение RecursionError\n",
    "        fact(-1)\n",
    "\n",
    "\n",
    "def fact(n):\n",
    "    '''\n",
    "    Реализация вычисления факториала.\n",
    "    '''\n",
    "    if n in range(0, 1):\n",
    "        return 1\n",
    "    return n * fact(n - 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Для запуска процесса тестирования необходимо указать в командной строке:\n",
    "\n",
    "```\n",
    "pytest fact.py\n",
    "```\n",
    "\n",
    "Тесты можно вынести в отдельный файл test_fact.py:\n",
    "\n",
    "```Python\n",
    "# test_fact.py\n",
    "import pytest\n",
    "from fact import fact\n",
    "\n",
    "\n",
    "def test_fact():\n",
    "    assert fact(5) == 120\n",
    "    assert fact(0) == 1\n",
    "    with pytest.raises(RecursionError):\n",
    "        fact(-1)\n",
    "```\n",
    "\n",
    "В этом случае для запуска тестирования достаточно набрать:\n",
    "\n",
    "```\n",
    "pytest\n",
    "```\n",
    "\n",
    "В результате будет выведено:\n",
    "\n",
    "```\n",
    "plugins: hypothesis-5.41.4\n",
    "collected 1 item\n",
    "\n",
    "test_fact.py .                                                           [100%]\n",
    "```\n",
    "\n",
    "Если же исправить одно из утверждений на `assert fact(6) == 120`, будет получен следующий результат:\n",
    "\n",
    "```\n",
    "plugins: hypothesis-5.41.4\n",
    "collected 1 item\n",
    "\n",
    "test_fact.py F                                                           [100%]\n",
    "\n",
    "================================== FAILURES ===================================\n",
    "__________________________________ test_fact __________________________________\n",
    "\n",
    "    def test_fact():\n",
    ">       assert fact(6) == 120\n",
    "E       assert 720 == 120\n",
    "E        +  where 720 = fact(6)\n",
    "\n",
    "test_fact.py:6: AssertionError\n",
    "=========================== short test summary info ===========================\n",
    "FAILED test_fact.py::test_fact - assert 720 == 120\n",
    "```\n",
    "\n",
    "Обратите внимание, что в модуле pytest результат выполнения оператора `assert` является более информативным, чем в стандартном варианте Питона.\n",
    "\n",
    "При использовании pytest важно правильно именовать функции тестирования. Такие функции должны иметь префикс `test_`. Кроме того, если речь идет об отдельном файле с тестами, то его имя также должно содержать префикс `test_`. Благодаря этому соглашению вызов `pytest` позволяет автоматически найти и запустить все тесты из соответствующих файлов текущего каталога.\n",
    "\n",
    "Рассмотрим следующую реализацию класса стека:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Stack:\n",
    "    def __init__(self):\n",
    "        self.data = []\n",
    "    \n",
    "    def push(self, x):\n",
    "        self.data.append(x)\n",
    "\n",
    "    def dup(self):\n",
    "        self.data.append(self.data[-1])\n",
    "\n",
    "    def pop(self):\n",
    "        if self.data:\n",
    "            return self.data.pop()\n",
    "        raise RuntimeError(\"Stack underflow\")\n",
    "    \n",
    "    def swap(self):\n",
    "        self.data[-1], self.data[-2] = self.data[-2], self.data[-1] "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Тестирование стека может быть вынесено в отдельный файл:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pytest\n",
    "\n",
    "\n",
    "def test_stack1():     \n",
    "    s = Stack()\n",
    "    s.push(1)\n",
    "    s.push(2)\n",
    "    assert len(s.data) == 2\n",
    "\n",
    "\n",
    "def test_stack2():     \n",
    "    s = Stack()\n",
    "    s.push(1)\n",
    "    s.push(2)\n",
    "    s.pop()\n",
    "    s.pop()\n",
    "    assert len(s.data) == 0\n",
    "\n",
    "\n",
    "def test_stack3():     \n",
    "    s = Stack()\n",
    "    s.push(1)\n",
    "    s.push(2)\n",
    "    s.swap()\n",
    "    assert s.data[-2:] == [2, 1]\n",
    "\n",
    "\n",
    "def test_stack4():\n",
    "    s = Stack()\n",
    "    with pytest.raises(RuntimeError):\n",
    "        s.pop()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Здесь имеет место дублирование кода, от которого в процедурах тестирования лучше избавляться. В противном случае автоматические тесты будет тяжело поддерживать и в них легко можно будет допустить ошибку. В нашем случае создание стека полезно выделить в отдельную настроечную функцию с помощью декоратора `@pytest.fixture`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "@pytest.fixture\n",
    "def stack():\n",
    "    s = Stack()\n",
    "    s.push(1)\n",
    "    s.push(2)\n",
    "    return s    \n",
    "\n",
    "\n",
    "@pytest.fixture\n",
    "def empty_stack():\n",
    "    return Stack()\n",
    "\n",
    "\n",
    "def test_stack1(stack):\n",
    "    assert len(stack.data) == 2\n",
    "\n",
    "\n",
    "def test_stack2(stack):     \n",
    "    stack.pop()\n",
    "    stack.pop()\n",
    "    assert len(stack.data) == 0\n",
    "\n",
    "\n",
    "def test_stack3(stack):\n",
    "    stack.swap()\n",
    "    assert stack.data[-2:] == [2, 1]\n",
    "\n",
    "\n",
    "def test_stack4(empty_stack):\n",
    "    with pytest.raises(RuntimeError):\n",
    "        empty_stack.pop()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "В коде выше аргументом у функций тестирования должно быть имя fixture-функции. Каждый раз при вызове функции тестирования будет вызвана функция `stack` или `empty_stack`, при этом создается новый экземпляр тестового стека.\n",
    "\n",
    "Еще большего сокращения кода тестирования можно достичь с помощью параметризации:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "@pytest.mark.parametrize('op1,op2,data', [\n",
    "    ('dup', 'pop', [1, 2]),\n",
    "    ('dup', 'dup', [1, 2, 2, 2]),\n",
    "    ('pop', 'pop', []),\n",
    "    ('swap', 'dup', [2, 1, 1]),\n",
    "])\n",
    "def test_stack5(stack, op1, op2, data):\n",
    "    getattr(stack, op1)()\n",
    "    getattr(stack, op2)()\n",
    "    assert stack.data == data"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Здесь используется декоратор `@pytest.mark.parametrize` для указания наборов значений аргументов функции тестирования."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Для реализации макетного тестирования может использоваться предопределенная fixture-функция monkeypatch. В примере ниже с ее помощью имитируется работа системной функции `input`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "def func():\n",
    "    x = input('Введите x:')\n",
    "    y = input('Введите y:')\n",
    "    return x + y\n",
    "\n",
    "\n",
    "def test_func(monkeypatch):\n",
    "    inputs = [1, 2]\n",
    "\n",
    "    def my_input(x):\n",
    "        return inputs.pop()\n",
    "\n",
    "    # До завершения работы test_func() функция input() будет переопределена\n",
    "    monkeypatch.setattr('builtins.input', my_input)\n",
    "    assert func() == 3"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Метрики покрытия кода\n",
    "\n",
    "Покрытие кода (Code coverage) используется при тестировании белого ящика и отражает ту часть программного кода, которая была выполнена в процессе работы набора тестовых сценариев. Информация о покрытии кода образуется в результате исполнения программного кода в режиме со сбором статистики о выполняемых командах.\n",
    "\n",
    "Различают следующие основные метрики покрытия кода:\n",
    "\n",
    "1. Покрытие операторов программы.\n",
    "1. Покрытие ветвей программы (переходов между парой операторов).\n",
    "\n",
    "Покрытие кода выражается в процентах и вычисляется, как отношение числа выполненнных операторов (пройденных ветвей) к общему количеству операторов (ветвей) в программе.\n",
    "\n",
    "Для оценки покрытия кода может быть использован сторонний модуль [coverage](https://coverage.readthedocs.io/en/coverage-5.5/):\n",
    "\n",
    "```\n",
    "pip install coverage\n",
    "```\n",
    "\n",
    "Рассмотрим следующий пример:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "def incr(x):\n",
    "    if x != 10:\n",
    "        x += 1\n",
    "    return x\n",
    "\n",
    "\n",
    "def test_incr():\n",
    "    assert incr(0) == 1"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Получить результат тестового покрытия можно следующей командой:\n",
    "\n",
    "```\n",
    "coverage run -m pytest inc.py\n",
    "```\n",
    "\n",
    "Результат (используя `coverage report`) может обескуражить:\n",
    "\n",
    "```\n",
    "Name    Stmts   Miss  Cover\n",
    "---------------------------\n",
    "my.py       6      0   100%\n",
    "---------------------------\n",
    "TOTAL       6      0   100%\n",
    "```\n",
    "\n",
    "Очевидно, что наш тест не покрывает все возможные варианты выполнения incr. Здесь более полезна метрика покрытия ветвей программы:\n",
    "\n",
    "```\n",
    "coverage run --branch -m pytest inc.py\n",
    "```\n",
    "\n",
    "Теперь видно, что покрытие неполное:\n",
    "\n",
    "```\n",
    "Name    Stmts   Miss Branch BrPart  Cover\n",
    "-----------------------------------------\n",
    "my.py       6      0      2      1    88%\n",
    "-----------------------------------------\n",
    "TOTAL       6      0      2      1    88%\n",
    "```\n",
    "\n",
    "100% покрытия легко добиться с помощью еще одного assert."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Мутационное тестирование\n",
    "\n",
    "Результат 100% покрытия кода не гарантирует отсутствия ошибок в программе. Один и тот же оператор программы может быть выполнен с разными наборами данных и в одном из непроверенных случаев может, к примеру, произойти деление на нуль.\n",
    "\n",
    "В этой связи полезно применять мутационное тестирование (Mutation testing, еще один вариант тестирования белого ящика), суть которого в привнесении ошибок (\"мутаций\") в исходную программу (тем самым создаются \"программы-мутанты\"), с тем, чтобы оценить, сможет ли существующий набор тестов эти ошибки определить. Если набор тестов успешно выполняется на программе-мутанте, то это означает, что используемые тесты нуждаются в развитии.\n",
    "\n",
    "Ниже представлен код вычисления евклидова расстояния и функция тестирования:\n",
    "\n",
    "```Python\n",
    "# Файл dist.py\n",
    "\n",
    "import math\n",
    "\n",
    "def dist(x1, y1, x2, y2):\n",
    "    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "```\n",
    "\n",
    "```Python\n",
    "# Файл test_dist.py\n",
    "\n",
    "from dist import dist\n",
    "\n",
    "def test_dist():\n",
    "    assert dist(4, 4, 4, 4) == 0\n",
    "```\n",
    "\n",
    "Вызов coverage сообщает о 100% покрытии:\n",
    "\n",
    "```\n",
    "Name           Stmts   Miss Branch BrPart  Cover\n",
    "------------------------------------------------\n",
    "dist.py            3      0      0      0   100%\n",
    "test_dist.py       3      0      0      0   100%\n",
    "------------------------------------------------\n",
    "TOTAL              6      0      0      0   100%\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Попробуем теперь использовать библиотеку [mutmut](https://mutmut.readthedocs.io/en/latest/) для мутационного тестирования `dist.py`. Устанавливается библиотека следующей командой:\n",
    "\n",
    "```\n",
    "pip install mutmut\n",
    "```\n",
    "\n",
    "После настройки конфигурационного файла `setup.cfg` запуск мутационного тестирования осуществляется командой `mutmut run`. Оказывается, \"выжило\" 5 программ-мутантов. Их текст можно вывести командой `mutmut show all`:\n",
    "\n",
    "```\n",
    "# mutant 22\n",
    "--- .\\dist.py\n",
    "+++ .\\dist.py\n",
    "@@ -1,5 +1,5 @@\n",
    " import math\n",
    "\n",
    " def dist(x1, y1, x2, y2):\n",
    "-    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "+    return math.sqrt((x1 - x2) * 2 + (y1 - y2) ** 2)\n",
    "\n",
    "\n",
    "# mutant 23\n",
    "--- .\\dist.py\n",
    "+++ .\\dist.py\n",
    "@@ -1,5 +1,5 @@\n",
    " import math\n",
    "\n",
    " def dist(x1, y1, x2, y2):\n",
    "-    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "+    return math.sqrt((x1 - x2) ** 3 + (y1 - y2) ** 2)\n",
    "\n",
    "\n",
    "# mutant 24\n",
    "--- .\\dist.py\n",
    "+++ .\\dist.py\n",
    "@@ -1,5 +1,5 @@\n",
    " import math\n",
    "\n",
    " def dist(x1, y1, x2, y2):\n",
    "-    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "+    return math.sqrt((x1 - x2) ** 2 - (y1 - y2) ** 2)\n",
    "\n",
    "\n",
    "# mutant 26\n",
    "--- .\\dist.py\n",
    "+++ .\\dist.py\n",
    "@@ -1,5 +1,5 @@\n",
    " import math\n",
    "\n",
    " def dist(x1, y1, x2, y2):\n",
    "-    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "+    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) * 2)\n",
    "\n",
    "\n",
    "# mutant 27\n",
    "--- .\\dist.py\n",
    "+++ .\\dist.py\n",
    "@@ -1,5 +1,5 @@\n",
    " import math\n",
    "\n",
    " def dist(x1, y1, x2, y2):\n",
    "-    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 2)\n",
    "+    return math.sqrt((x1 - x2) ** 2 + (y1 - y2) ** 3)\n",
    "```\n",
    "\n",
    "Для этих программ-мутантов pytest сигнализирует об успешном прохождении тестирования. Очевидно, что следующим шагом ожидается доработка набора тестов, чтобы избавиться от мутантов."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Контрактное программирование\n",
    "\n",
    "В контрактном программировании (Design by contract) интерфейсы программных компонентов (таких, например, как функции или методы) получают формальные спецификации. Эти спецификации или, иначе, контракты включают в себя:\n",
    "\n",
    "1. Предусловия. Предикаты, которые должны быть истинными на входе в программный компонент. \n",
    "2. Постусловия.  Предикаты, которые должны быть истинными при выходе из программного компонента.\n",
    "3. Инварианты. Предикаты, которые должны быть истинными в пределах программного компонента.\n",
    "4. Указание побочного эффекта. Различные типы побочного эффекта включают в себя ввод/вывод и модификацию глобальных данных.\n",
    "\n",
    "Контракты проверяются, в основном, во время выполнения программы и по этой причине являются более выразительными, чем статические системы типов.\n",
    "\n",
    "В Питоне для реализации контрактного программирования имеется сторонняя библиотека [deal](https://deal.readthedocs.io/), которую можно установить следующим образом:\n",
    "\n",
    "```\n",
    "pip install deal\n",
    "```\n",
    "\n",
    "Для изучения контрактного программирования с deal используем следующую функцию:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(3, 1)"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def divrem(q, p):\n",
    "    '''\n",
    "    Функция divrem возвращает частное и остаток от деления.\n",
    "    '''\n",
    "    d = 0\n",
    "    if p == 0:\n",
    "        raise ZeroDivisionError\n",
    "    while q >= p:\n",
    "        q -= p\n",
    "        d += 1\n",
    "    return d, q\n",
    "\n",
    "divrem(10, 3)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Добавим теперь пред- (декоратор `@deal.pre`) и постуловия (декоратор `@deal.post`):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pytest\n",
    "import deal\n",
    "\n",
    "\n",
    "@deal.pre(lambda q, p: q >= 0 and p >= 0)\n",
    "@deal.post(lambda result: result[0] >= 0 and result[1] >= 0)\n",
    "def divrem(q, p):\n",
    "    '''\n",
    "    Функция divrem возвращает частное и остаток от деления.\n",
    "    '''\n",
    "    d = 0\n",
    "    if p == 0:\n",
    "        raise ZeroDivisionError\n",
    "    while q >= p:\n",
    "        q -= p\n",
    "        d += 1\n",
    "    return d, q\n",
    "\n",
    "\n",
    "def test_divrem():\n",
    "    divrem(10, 5)\n",
    "    with pytest.raises(ZeroDivisionError):\n",
    "        divrem(0, 0)\n",
    "    divrem(0, 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Здесь `lambda` обозначает создание безымянной функции (к таким функциям мы еще вернемся в следующей лекции).\n",
    "\n",
    "Запуск тестирования с помощью `pytest` сигнализирует об успехе. Теперь добавим еще один вариант постусловия (@deal.ensure), в котором используются как аргументы, так и результат:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "@deal.pre(lambda q, p: q >= 0 and p >= 0)\n",
    "@deal.post(lambda result: result[0] >= 0 and result[1] >= 0)\n",
    "@deal.ensure(lambda q, p, result: result == (q // p, q % p))\n",
    "def divrem(q, p):\n",
    "    '''\n",
    "    Функция divrem возвращает частное и остаток от деления.\n",
    "    '''\n",
    "    d = 0\n",
    "    if p == 0:\n",
    "        raise ZeroDivisionError\n",
    "    while q >= p:\n",
    "        q -= p\n",
    "        d += 1\n",
    "    return d, q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Наконец, мы можем добавить для функции `divrem` контракты, указывающие на вызываемое исключение (`@deal.raises`), его причину (`@deal.reason`), а также информацию о побочном эффекте (`@deal.has`):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "@deal.pre(lambda q, p: q >= 0 and p >= 0)\n",
    "@deal.post(lambda result: result[0] >= 0 and result[1] >= 0)\n",
    "@deal.ensure(lambda q, p, result: result == (q // p, q % p))\n",
    "@deal.reason(ZeroDivisionError, lambda q, p: p == 0)\n",
    "@deal.raises(ZeroDivisionError)\n",
    "@deal.has()\n",
    "def divrem(q, p):\n",
    "    '''\n",
    "    Функция divrem возвращает частное и остаток от деления.\n",
    "    '''\n",
    "    d = 0\n",
    "    if p == 0:\n",
    "        raise ZeroDivisionError\n",
    "    while q >= p:\n",
    "        q -= p\n",
    "        d += 1\n",
    "    return d, q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Обратите внимание, что при вызове не указанного в контракте исключения будет выдана специальная ошибка.\n",
    "\n",
    "В нашем случае у функции отсутствует побочный эффект. Если бы внутри `divrem` содержался вызов `print`, то побочный эффект можно было бы указать явно: `@deal.has('stdout')`. Когда некоторая функция вызывает функцию с заданным побочным эффектом, то для вызывающей функции необходимо также сделать пометку о наличии этого побочного эффекта.\n",
    "\n",
    "В deal существует инвариант класса (`@deal.inv`), который проверяется при входе и выходе из методов, а также при изменении атрибутов объекта:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "@deal.inv(lambda account: account.money >= 0)\n",
    "class Account:\n",
    "    def __init__(self):\n",
    "        self.money = 0\n",
    "\n",
    "    def get(self, amount):\n",
    "        self.money -= amount\n",
    "\n",
    "    def put(self, amount):\n",
    "        self.money += amount\n",
    "\n",
    "\n",
    "a = Account()\n",
    "\n",
    "a.put(10)\n",
    "a.get(10)\n",
    "# Раскомментируйте следующую строку, чтобы получить ошибку контракта\n",
    "# a.money -= 20\n",
    "a.money"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Тестирование на основе свойств\n",
    "\n",
    "Тестирование на основе свойств (Property-based testing) основно на использовании нескольких мощных техник:\n",
    "\n",
    "1. Тестирование на случайных структурированных входных данных или \"фаззинг\" ([fuzzing](https://www.fuzzingbook.org/)).\n",
    "2. Сокращение контрпримера с помощью [дельта-отладки](https://www.debuggingbook.org/beta/html/DeltaDebugger.html#General-Delta-Debugging) и подобных подходов.\n",
    "3. Тестирование на основе модели (Model-based testing) для тестирования систем с состоянием.\n",
    "\n",
    "Процесс тестирования на основе свойств включает в себя описание типов случайных входных данных и определение ключевых свойств-предикатов, которые характеризуют тестируемый программный компонент. Тестирующая система автоматически находит контрпримеры в виде случайно сгенерированных входных данных, на которых заданные свойства не выполняются, после чего пользователю выдается наиболее краткий вариант контрпримера.\n",
    "\n",
    "Для дальнейшей работы понадобится сторонняя библиотека hypothesis, которую можно установить следующей командой:\n",
    "\n",
    "```\n",
    "pip install hypothesis\n",
    "```\n",
    "\n",
    "В примере ниже тестируется функция сложения. Декоратор `@given` служит для описания случайных тестовых входов. Типы случайных данных определяются стратегиями. В данном случае используется стратегия `integers`, которая позволяет генерировать случайные целые значения. В примере проверяются свойства коммутативности и ассоциативности сложения:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "from hypothesis import given, strategies as st\n",
    "\n",
    "\n",
    "def add(x, y):\n",
    "    return x + y\n",
    "\n",
    "\n",
    "@given(x=st.integers(), y=st.integers(), z=st.integers())\n",
    "def test_add(x, y, z):\n",
    "    assert add(x, y) == add(y, x)\n",
    "    assert add(x, add(y, z)) == add(add(x, y), z)\n",
    "\n",
    "    \n",
    "test_add()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "В следующем примере используется параметризованная стратегия `lists` для порождения случайных списков:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Вернуть наиболее часто встречающийся элемент\n",
    "def mode(data):\n",
    "    return max(data, key=data.count)\n",
    "\n",
    "\n",
    "@given(data=st.lists(st.integers()))\n",
    "def test_mode(data):\n",
    "    assert mode(data) in data\n",
    "\n",
    "    \n",
    "# test_mode()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Если раскомментировать последнюю строку, то будет выдан контрпример в виде пустого списка:\n",
    "    \n",
    "```\n",
    "Falsifying example: test_mode(\n",
    "    data=[],\n",
    ")\n",
    "```\n",
    "\n",
    "Изменим генерацию случайных списков и добавим еще одно свойство (количество вхождений результата должно быть больше или равно количеству вхождений любого из элементов списка). В этом примере используется функция `all` которая возвращает True, если все элементы последовательности интерпретируются, как True:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Вернуть наиболее часто встречающийся элемент\n",
    "def mode(data):\n",
    "    return max(data, key=data.count)\n",
    "\n",
    "\n",
    "@given(data=st.lists(st.integers(), min_size=1))\n",
    "def test_mode(data):\n",
    "    res = mode(data)\n",
    "    assert res in data\n",
    "    assert all(data.count(res) >= data.count(x) for x in data)\n",
    "    \n",
    "\n",
    "test_mode()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "При желании, с помощью добавления `print`, можно посмотреть на то, какие именно данные поступают на вход `test_mode`:\n",
    "\n",
    "```\n",
    "...\n",
    "[25963, -1, -18826]\n",
    "[129, -1, -18826]\n",
    "[-384, -386, -18826]\n",
    "[-384, -386, -18826]\n",
    "[-12350, -13880, -1741946127877086248, 27900318018340847272440741409395352381, 1640638466, -29885, 16118, 83, -30, 7112358378030895761, 76]\n",
    "[0, -25099, 115, 0, -3325696608601645481337506961643569664, -25099, 115, 3, 1640638466, -29885, 16118, 83, -30, 7112358378030895761, 76]\n",
    "[-13150, -30569]\n",
    "[51, 1]\n",
    "...\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Ниже показан пример с использованием стратегии `recursive` в которой первый аргумент указывает на базовый случай-стратегию, а вторым аргументом является функция, принимающая и возвращающая стратегию:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [],
   "source": [
    "class List:\n",
    "    def __init__(self, x, right=None):\n",
    "        self.x = x\n",
    "        self.right = right\n",
    "    \n",
    "    def __repr__(self):\n",
    "        return f'[{self.x}] -> {self.right}'\n",
    "    \n",
    "    def __len__(self):\n",
    "        size = 1\n",
    "        while self.right:\n",
    "            size += 1\n",
    "            self = self.right\n",
    "        return size\n",
    "    \n",
    "    def get_last(self):\n",
    "        while self.right:\n",
    "            self = self.right\n",
    "        return self\n",
    "    \n",
    "    def add(self, x):\n",
    "        self.get_last().right = List(x)\n",
    "           \n",
    "\n",
    "@given(lst=st.recursive(st.builds(List, st.integers()),\n",
    "                        lambda r: st.builds(List, st.integers(), r)),\n",
    "                       x=st.integers())\n",
    "def test_list(lst, x):\n",
    "    size = len(lst)\n",
    "    lst.add(x)\n",
    "    assert len(lst) == size + 1\n",
    "    assert lst.get_last().x == x\n",
    "\n",
    "\n",
    "test_list()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Вот как выглядят примеры случайно формируемых списков:\n",
    "\n",
    "```\n",
    "...\n",
    "[0] -> [0] -> None\n",
    "[25275] -> [-37] -> [22] -> None\n",
    "[0] -> [384] -> [-1] -> None\n",
    "[25181955] -> [3597652295274685506] -> [51] -> None\n",
    "[0] -> [-28743] -> [-51] -> [2] -> [1] -> None\n",
    "[31214] -> [-21250] -> [126] -> [15226] -> None\n",
    "[0] -> [0] -> None\n",
    "[-17840] -> [114] -> None\n",
    "[68] -> None\n",
    "[30564] -> [69258178314550572426917407876740709799] -> [-1670540173] -> None\n",
    "...\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Тестирование на основе свойств можно комбинировать с контрактным программированием. Далее показан вариант программы из предыдущего раздела с использованием библиотек `deal` и `hypothesis`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [],
   "source": [
    "@deal.pre(lambda q, p: q >= 0 and p >= 0)\n",
    "@deal.post(lambda result: result[0] >= 0 and result[1] >= 0)\n",
    "@deal.ensure(lambda q, p, result: result == (q // p, q % p))\n",
    "@deal.reason(ZeroDivisionError, lambda q, p: p == 0)\n",
    "@deal.raises(ZeroDivisionError)\n",
    "@deal.has()\n",
    "def divrem(q, p):\n",
    "    d = 0\n",
    "    if p == 0:\n",
    "        raise ZeroDivisionError\n",
    "    while q >= p:\n",
    "        q -= p\n",
    "        d += 1\n",
    "    return d, q\n",
    "\n",
    "\n",
    "@given(x=st.integers(min_value=0, max_value=100), y=st.integers(min_value=1, max_value=100))\n",
    "def test_divrem(x, y):\n",
    "    divrem(x, y)\n",
    "\n",
    "\n",
    "test_divrem()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Важно использовать такие свойства, которые позволят как можно полнее верифицировать тестируемую систему. Были [предложены](https://fsharpforfunandprofit.com/posts/property-based-testing-2/) следующие основные категории свойств:\n",
    "\n",
    "1. **Разные пути, одна цель**. Различный порядок действий приводит к одному и тому же результату. Пример: проверка коммутативности и ассоциатиновности.\n",
    "1. **Туда и обратно**. После совершения операции, за которой следует обратная операция, должен быть получен исходный результат. Пример: сжатие и расжатие данных.\n",
    "1. **Некоторые вещи не меняются**. Элементы, которых не затрагивает преобразование, должны остаться на своих местах. Пример: после сортировки не должен измениться размер списка и из списка не должны пропасть какие-то элементы.\n",
    "1. **Чем больше вещи меняются, тем больше они остаются прежними**. Повторное применение некоторых операций уже не должно влиять на результат. Пример: последовательность GET-запросов к HTTP-серверу (если данные не изменились) должна соответствовать единственному такому запросу.\n",
    "1. **Сначала решить меньшую проблему** или **Разделяй и властвуй**. Сначала проверить некоторое свойство для простого режима системы. Пример: проверка работы операции для пустого списка или пустого дерева.\n",
    "1. **Трудно доказать, легко проверить**. Здесь имеется отсылка к NP-полным задачам, найти решение для которых значительно сложнее, чем проверить корректность полученного решения. Пример: найти выход из лабиринта может быть сложно, а проверить, что путь приводит к выходу значительно легче.\n",
    "1. **Тестовый оракул**. Во многих случаях уже существует эталонная система, поведение которой можно сравнить с тестируемой системой. Пример: в функции `divrem` для проверки контракта использовались встроенные операции деления и взятия остатка.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "В заключение рассмотрим тестирование на основе модели, которое представляет собой вариант \"тестового оракула\". В следующем примере мы рассматриваем тестируемую систему, как реактивную. Тестируются последовательности операций над низкоуровневой реализацией стека и ее моделью, с использованием формализма конечного автомата:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [],
   "source": [
    "from hypothesis.stateful import Bundle, RuleBasedStateMachine, rule, precondition\n",
    "\n",
    "\n",
    "class Stack:\n",
    "    def __init__(self, size):\n",
    "        self.data = [0] * size\n",
    "        self.sp = 0\n",
    "   \n",
    "    def push(self, x):\n",
    "        self.data[self.sp] = x\n",
    "        self.sp += 1\n",
    "\n",
    "    def get_top(self):\n",
    "        return self.data[self.sp - 1]\n",
    "\n",
    "    def dup(self):\n",
    "        self.push(self.get_top())\n",
    "        \n",
    "    def pop(self):\n",
    "        x = self.get_top()\n",
    "        self.sp -= 1\n",
    "        return x\n",
    "    \n",
    "    def swap(self):\n",
    "        y, x = self.pop(), self.pop()\n",
    "        self.push(x)\n",
    "        self.push(y)\n",
    "\n",
    "\n",
    "class ModelStack(RuleBasedStateMachine):\n",
    "    def __init__(self):\n",
    "        super().__init__()\n",
    "        self.data = []\n",
    "        self.stack = Stack(100)\n",
    "\n",
    "    @rule(x=st.integers())\n",
    "    def push(self, x):\n",
    "        self.stack.push(x)\n",
    "        self.data.append(x)\n",
    "\n",
    "    @rule()\n",
    "    @precondition(lambda self: len(self.data))\n",
    "    def dup(self):\n",
    "        self.stack.dup()\n",
    "        self.data.append(self.data[-1])\n",
    "\n",
    "    @rule()\n",
    "    @precondition(lambda self: len(self.data))\n",
    "    def pop(self):\n",
    "        self.stack.pop()        \n",
    "        return self.data.pop()\n",
    "          \n",
    "    @rule()\n",
    "    @precondition(lambda self: len(self.data) > 1)\n",
    "    def swap(self):\n",
    "        self.stack.swap()\n",
    "        self.data[-1], self.data[-2] = self.data[-2], self.data[-1]\n",
    "\n",
    "    @rule()\n",
    "    def check_stacks(self):\n",
    "        assert self.stack.data[:self.stack.sp] == self.data\n",
    "\n",
    "\n",
    "test_stack = ModelStack.TestCase"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Здесь `@rule` определяет состояние конечного автомата, а `@precondition` определяет условие выполнения перехода в заданное состояние.\n",
    "\n",
    "Запуск `pytest` выдает следующий контрпример:\n",
    "\n",
    "```Python\n",
    "state = ModelStack()\n",
    "state.push(x=0)\n",
    "state.push(x=1)\n",
    "state.swap()\n",
    "state.check_stacks()\n",
    "state.teardown()\n",
    "```\n",
    "\n",
    "Очевидно, что в реализации операции swap имеется ошибка. После ее исправления тесты на основе модели проходят успешно."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.10.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}