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