Почему глючат программы

Большинство из нас периодически сталкивается с тем, что программное обеспечение, которое мы используем, работает не так как нам кажется, оно должно. В некоторых случаях мы просто принимаем желаемое за действительное и программа работает так, как задумал программист, хотя нам это не нравится или логика не очевидна. Но в некоторых случаях (чаще, чем хотелось бы), нелогичное поведение программы - результат ошибки программиста. И мы ругаем про себя (а некоторые и вполне себе громко, отчётливо и внятно) неизвестных нам индусов, резонно полагая, что проблемы - результат недостаточной квалификации программистов и лени тестировщиков.

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

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

Технология носит название "доказательное программирование" и в настоящее время применяется в системах, где отсутствие ошибок критично. К примеру компания Airbus проектирует ПО и электронное оборудование для транспорта и авиации с помощью методов "доказательства" или, иначе, верификации программ.

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

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

Но и это ещё не всё! Для окончательной, железобетонной уверенности, что всё будет работать, нужно верифицировать компилятор, который выдаст исполняемый код. А также процессор, на котором этот код будет исполняться. Но идеал, увы, редко достижим...

Тем не менее, существуют проекты, развивающиеся именно по этой технологии. Как пример, можно привести работу команды программистов из компании "NICTA", которые с 2009го года занимаются верификацией кода микроядра Linux, доказывая отсутствие ошибок определённого вида (в первую очередь, утечек памяти и нарушения привилегий). Одним из первых был верифицирован код полностью автоматического управления одной из линий Парижского метро (1988).

Более того, в 2003 году стартовал проект разработки верифицирующего компилятора - т. е. такого, который будет выдавать уже проверенный исполняемый код. Для его поддержки создана и пополняется библиотека верифицированных модулей и алгоритмов (Verified Software Repository).

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

А оттуда недалеко уже и до автоматического создания готовых программ для решения возникающих задач по мере их появления... и где-то на горизонте замаячил Скайнет...

Ссылки на дополнительные материалы:
http://mk.cs.msu.ru/images/e/ee/Lecture_Verification_1.pdf - лекция о методах верификации
https://www.cs.ox.ac.uk/files/6187/Grand.pdf - описание проекта верифицирующего компилятора
http://vsr.sourceforge.net/ - Verified Software Repository
https://goo.gl/qJGFr3 - статья о верификации в Википедии

Иллюстрации - https://www.pexels.com