Курсовая работа: Метод применения теории типов Мартина-Лёфа для верификации программных систем

Оглавление

• Изоморфизм Карри-Говарда и зависимые типы . . . . . . . . . . . . . . 7

• Языки программирования с зависимыми типами . . . . . . . . . . . . . 11

• ОсобенностиCиA.......................... 12

• Легковесное верифицирование с помощью зависимых типов . . . . . . 14

• Верифицирование сложных систем . . . . . . . . . . . . . . . . . . . . . 15 3.2. Инструмент экстракции J -кода по C -спецификации . . . . . . . . . 18

§ Трансляция алгебраических типов данных . . . . . . . . . . . . . . . . 19

• Трансляция функций как значений первого порядка . . . . . . . . . . . 20

3

Введение

Важная проблема при разработке программного обеспечения гарантия его кор-ректности, то есть тщательная формулировка желаемых свойств продукта с после-дующей их проверкой. Обычно, эта задача решается неформально в процессе реали-зации программы; но с ростом объёма работы уследить за всевозможными нюансами реализации становится трудно, ошибки неизбежно происходят.

Подобные ошибки могут годами оставаться незамеченными, уже после выпуска продукта и на стадии поддержки. Особо дорогие ошибки могут стоить пользователю или заказчику до сотен миллионов долларов.

Проблема корректности ПО становится ещё более актуальной с учётом нескольких тенденций: количественного возрастания размера программных систем и их переме-щения из “локального” пространства пользователя в “глобальное”.

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

Если абстрагироваться от конкретных примеров, то централизация проявляется:

• во времени пользователи работают одновременно;

• логически действия пользователей взаимосвязаны между собой;

• физически вычисления производятся одним и тем же вычислителем, а данные часто хранятся на одном носителе информации.

Кроме повышенного параллелизма это влечёт за собой и бóльшую скорость и об-ласть распространения изменений. К примеру, в онлайн сервисах изменение кода мо-жет выпуститься за пару дней, десктопные приложения тоже могут автоматически обновиться через сеть; если обновление содержит ошибку, то она затрагивает сразу множество компьютеров, также и незамеченные уязвимости подвергают риску взлома сразу всех пользователей.

Таким образом, к программным системам, работающим с большим количеством пользователей в одном пространстве, предъявляются повышенные требования кор-ректности и целесообразно применять формальные методы проверки. Одним из таких методов является формальная верификация автоматизированная проверка продук-та на соответствие