Практикум -- задание №2
Это задание состоит из 2-х частей. Нужно выполнить все части.
Задание 2.1
При помощи Why3 и солверов докажите, что для любого
целого неотрицательного n
значение выражения
23n - 3n
делится
без остатка на 5. Использовать циклы нельзя. Для этого:
-
Определите функцию взятия в степень, которая будет использоваться только в спецификациях.
-
Запишите let-функцию со спецификацией, чтобы из полной корректности этой пары следовало требуемое утверждение.
-
Докажите требуемое утверждение «на листочке».
-
Если нужно, можете добавить функций и лемм.
-
Результат вашей работы – это архив следующего состава: файл на языке WhyML, сессия доказательства.
Прагматика Это задание знакомит вас с языком WhyML, с доказательством полной корректности рекурсивных функций.
Задание 2.2
Реализуйте алгоритм «Решето Эратосфена» и докажите полную корректность своей реализации. Для этого:
-
Опишите полиморфный тип-символ для множества. Опишите val-примитивы для константы - пустого множества, добавления числа во множество, удаления числа из множества. Опишите функциональные и предикатные символы, необходимые для спецификации алгоритма и val-примитивов. Добавьте спецификации val-примитивам. Опишите аксиомы для символов.
-
Опишите let-функцию, получающую целое положительное число и возвращающую множество всех простых чисел, не превышающих этого числа. Опишите ее спецификацию. Функциональные и предикатные символы можно использовать только для спецификации. При желании можно добавить let-функции. val-примитивы не добавляйте.
-
Докажите полную корректность своей let-функции относительно ее спецификации. При необходимости добавляйте леммы и лемма-функции.
-
Результат вашей работы – это архив следующего состава: файл на языке WhyML, сессия доказательства.
Прагматика Это задание позволяет отработать спецификацию логических символов и отработать методы Флойда на более сложной модели программы.