У меня вдруг родилась вот какая идея. Известно, что корректную программу написать проще, если сначала формально вывести алгоритм, доказать его правильность (т.е. достижимость конечной цели и отсутствие нежелательных побочных эффектов), а затем вывести из формального определения алгоритма конкретный исходный текст программы. На этом пути есть несколько моментов, допускающих человеческую ошибку:
- доказательство правильности алгоритма может быть проведено некорректно;
- в процессе перевода алгоритма из формальной спецификации в текст на конкретном языке программирования могут быть допущены неточности или ошибки;
- особенности языка программирования могут давать побочные эффекты или вносить коррективы, не учтенные в формальной спецификации, потенциально нарушая целостность программы и её соответствие алгоритму (например, переполнение INTEGER в некоторых промежуточных вычислениях).
Почему бы нам не автоматизировать процесс перевода формальной спецификации в текст программы?
Почитав немного о языках логического программирования (например, Prolog) я обнаружил, что на таком языке можно было бы написать спецификацию, т.е. требования к пред-, постусловиям и инвариантам. Далее интерпретатор, имея некую базу знаний об алгоритмах с их пред- и постусловиями, мог бы найти решение либо констатировать отсутствие необходимой информации. В случае успешного поиска решения интерпретатор мог бы сгенерировать исходный текст на целевом императивном языке программирования (например, Oberon-2). Полученный исходный текст имел бы заранее известные, доказуемые свойства.
Дальше ещё интереснее. Если спецификация меняется, как это часто бывает в процессе интерактивной разработки, транслятор автоматически сообщает нам, где и какие предположения оказываются нарушенными. А если возможно, то даже ничего не сообщает, а просто генерирует новый код, полностью соответствующий новой спецификации - от низкоуровневых библиотек до "бизнес-логики".
Такие товарищи как Т. Хоар пытаются создать верифицирующий компилятор. Это очень большая и сложная задача, особенно если компилировать Си или ассемблер. А что, если пойти не со стороны анализа, а со стороны синтеза? Не искать смысл в написанном коде, а писать смысл, который будет автоматически отображаться в соответствующий код.
Хотелось бы услышать мнение людей, чей кругозор не ограничивается парой-тройкой императивных языков (как у меня). Возможно ли это?
|
И работы в этом направлении проводились. С несколько более глобальной идеей столкнулся в книге "Концептуальное программирование", автор Тыугу Э.Х. - 1980-х годов: