OberonCore

Чем лексикон отличается от языка программирования? Он выражает не только и не столько программы, сколько их свойства и наши суждения о них. Язык программирования кодирует объекты предметной области задачи, а наше знание об этих объектах остается за пределами программного текста. Лексикон же является средством описания объектов предметных областей и содержит нотацию для построения баз знаний о предметных областях. Программа, выраженная средствами лексикона, в определенном смысле содержит в своем тексте описание своей семантики в виде совокупности нетривиальных фактов о вычисляемой ею функции – в отличие от "чистых" программ, которые не говорят ничего о своих функциональных свойствах.

Лексикон, в отличие от конкретного языка программирования, является открытой системой. Для него в целом не ставится задача трансляции любого его текста в машинную программу, хотя любая машинная программа в случае необходимости может быть выражена в лексиконе. Аналогично естественному языку лексикон обладает способностью описания одной своей части средствами другой своей же части.

Не надо думать, что лексикон – это все и навсегда. Это тщательно отобранная, но развивающаяся система удачных обозначений. Степень его успеха определяется степенью общезначимости и общепонятности его нотации.

Не надо думать, что лексикон – это все и навсегда. Это тщательно отобранная, но развивающаяся система удачных обозначений. Степень его успеха определяется степенью общезначимости и общепонятности его нотации.

...Конечно, здесь мы сознательно умалчиваем о более глубоких средствах: верификаторах и трансформаторах программ, но эти средства мы побережем для развития главной идеи.

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

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

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

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

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

В качестве основы лексикон содержит стандартную математическую символику алгебры, теории множеств, математической логики. В дополнение к ней лексикон содержит нотацию для основных конструкций и примитивов программирования на самых разных уровнях. Смысл этих конструкций сам выражается средствами лексикона. Лексикон содержит развитую систему именования и разнообразные правила подстановки.

С сегодняшнего времени смотря на те размышления Ершова, можно говорить о построении онтологии программирования. Или более широко - онтологии ИТ
То есть системы понятий и связей между ними.
Это и будет тот самый лексикон.
Конкретный язык программирования, естественно, не может претендовать на эту роль.

Мне кажется, что Андрей Петрович Ершов мыслил в рамках текстового (не визуального) программирования. Он представлял себе лексикон как чисто текстовую (не визуальную) систему.
Он умер в 1988 году и не мог предвидеть, что визуальные идеи (понимаемые как расширение текста с помощью графики) будут получать все более широкое распространение.

Тот факт, что он умело использовал графику при анализе схем Янова, не меняет дела. Не меняет в том смысле, что Андрей Петрович (как мне кажется) не допускал даже мысли, что со временем в состав лексикона — наряду с текстом — обязательно войдет графика.

С сегодняшнего времени смотря на те размышления Ершова, можно говорить о построении онтологии программирования. Или более широко - онтологии ИТ
То есть системы понятий и связей между ними.
Это и будет тот самый лексикон.
Конкретный язык программирования, естественно, не может претендовать на эту роль.

Языки спецификации свойств программ, в отличие от языков спецификации задач, должны быть приближены к соответствующим языка программирования высокого уровня (ADA, Паскаль, ПЛ/1 и др.), свойства конструкций который они должны характеризовать. Целесообразно рассматривать поэтому язык спецификации свойств программ как составную часть общей с языком программирования языковой среды (лексикона), используемой разработчиком программ.
Лексикон как смесь двух и более формальных языков, есть язык более высокого уровня, чем обычный язык программирования. Если на языке программирования описываются только обрабатываемая информация и процессы вычислений (алгоритм, реализующий задачу), то на языке спецификации свойств программ дополнительно может описываться метаинформация о программе - свойствах объектов программы и процессов вычислений по программе. Такая метаинформация представляется, как уже отмечалось в гл. 1, в виде контролирующих структур, сопровождающих программный текст и используемых в процессе разработки или (и) сопровождения программы, а иногда и в процессе выполнения программы.
Заметим, что спецификация свойств программы в процессе разработки поддерживает необходимую обратную связь между объектом разработки (программой) и спецификацией задачи (на языке функциональной спецификации), обеспечивая итеративный характер процесса разработки. Сопоставление спецификации задачи и спецификации свойств программы позволяет проводить коррекцию задачи или программы при последующих итерациях. Это создает основу для эффективных технологий надежного проектирования программ.
Наиболее развитыми возможностями обладают логические языки спецификации свойств программ. Они создаются обычно на базе логических выражений языка программирования, расширенных свойствами квантификации и аксиоматического определения новых понятий проблемной области. Элементами утверждений о свойствах программ обычно являются логические инварианты - формулы языка спецификации, связанные с соответствующими точками текста программы или объектами программы.

Специфицировать программу - это значит указать на достаточно высоком уровне абстракции, какими свойствами должно обладать ее выполнение. Достичь этого можно, записывая соответствующие формулы (спецификации) в тексте программы (перед или после отдельных фрагментов либо всей программы). Они являются утверждениями о том, что должно быть истинно в соответствующих точках программы. Указанные утверждения назовем индуктивными утверждениями.
Различие между спецификациями (индуктивными утверждениями) и инвариантами состоит в том, что индуктивные утверждения отражают лишь желаемые свойства, которые при наличии ошибок могут не соответствовать фактическим свойствам (инвариантам).
Программа с записанными индуктивными утверждениями о ней или ее фрагментах является аннотированной программой. Аннотированная программа - качественно новый объект по сравнению с обычной программой. Если обычная программа представляет лишь алгоритм решения задачи, то аннотированная - формальное утверждение о программе (алгоритме и, возможно, о данных программы). Это означает, что аннотированные программы можно рассматривать как некоторый специальный вид логических формул, способных принимать значения true или false.
Образно говоря, аннотированная программа - формула на лексиконе (язык программирования + логический язык спецификации). Такое ее рассмотрение открывает широкие возможности для формальных преобразований аннотированных программ и формальных доказательств свойств программ, что является основой для верификации и оптимизации программ. Аннотированные программы являются также ценным компонентом документации и могут эффективно использоваться в процессах отладки (тестирования) и контроля работы программы.

2.3 ЛОГИЧЕСКИЙ ЯЗЫК СПЕЦИФИКАЦИИ СВОЙСТВ ПРОГРАММ

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

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

С практической точки зрения логический язык спецификации свойств программ должен обладать следующими свойствами.

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

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

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

Г. Приближением нотации языка спецификации к естественному языку и используемому языку программирования, что необходимо также для обеспечения ясности спецификации и удобств работы с ними в процессе разработки программ.

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

Данную цитату, как мне кажется, можно считать определением лексикона программирования, в том смысле, как его понимал А.П. Ершов (цитата взята из книги "Практические методы верификации программ")

А в этой книге примеры есть на данную тему?

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

Я говорю о постоянно используемых «логических» структурах, которых совсем не много:

Список
Очередь (FIFO)
Стек (LIFO)
Дерево (разные деревья)
Ассоциативный массив
Хеш-таблица
Вектор (№-мерная матрица)

Вот это «золотой фонд» программирования. Это безусловно часть «Лексикона программирования», о котором говорил А.П. Ершов.

Да, смысл в том, чтобы не просто закрепить какие-то аксиомы для типа boolean, integer и все на этом, а в том, чтобы можно было добавлять новые понятия