Это задание состоит из 2-х частей. Нужно выполнить все части.

Задание 2.1

При помощи Why3 и солверов докажите, что для любого целого неотрицательного n значение выражения 23n - 3n делится без остатка на 5. Использовать циклы нельзя. Для этого:

  1. Определите функцию взятия в степень, которая будет использоваться только в спецификациях.

  2. Запишите let-функцию со спецификацией, чтобы из полной корректности этой пары следовало требуемое утверждение.

  3. Докажите требуемое утверждение «на листочке».

  4. Если нужно, можете добавить функций и лемм.

  5. Результат вашей работы – это архив следующего состава: файл на языке WhyML, сессия доказательства.

Прагматика Это задание знакомит вас с языком WhyML, с доказательством полной корректности рекурсивных функций.

Задание 2.2

Реализуйте алгоритм «Решето Эратосфена» и докажите полную корректность своей реализации. Для этого:

  1. Опишите полиморфный тип-символ для множества. Опишите val-примитивы для константы - пустого множества, добавления числа во множество, удаления числа из множества. Опишите функциональные и предикатные символы, необходимые для спецификации алгоритма и val-примитивов. Добавьте спецификации val-примитивам. Опишите аксиомы для символов.

  2. Опишите let-функцию, получающую целое положительное число и возвращающую множество всех простых чисел, не превышающих этого числа. Опишите ее спецификацию. Функциональные и предикатные символы можно использовать только для спецификации. При желании можно добавить let-функции. val-примитивы не добавляйте.

  3. Докажите полную корректность своей let-функции относительно ее спецификации. При необходимости добавляйте леммы и лемма-функции.

  4. Результат вашей работы – это архив следующего состава: файл на языке WhyML, сессия доказательства.

Прагматика Это задание позволяет отработать спецификацию логических символов и отработать методы Флойда на более сложной модели программы.