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