Данную цитату, как мне кажется, можно считать определением лексикона программирования, в том смысле, как его понимал А.П. Ершов (цитата взята из книги "Практические методы верификации программ"):
> -- Цитата:
> 2.3 ЛОГИЧЕСКИЙ ЯЗЫК СПЕЦИФИКАЦИИ СВОЙСТВ ПРОГРАММ	 Важнейшими качествами этого языка для задач верификации программ являются:	выразительная способность, т.е. возможность формально выражать широкий класс утверждений о свойствах и отношениях программных переменных;	дедуктивная способность, т.е. возможность формально доказывать истинность утверждений, выразимых в языке.	Следует иметь в виду, что оба эти качества формального языка спецификации не могут быть безграничны в своем приближении к естественному языку и к неформальным способам рассуждений. Для этого достаточно богатого формального логического языка существуют как невыразимые утверждения естественного языка, так и недоказуемы (но истинные) формальные утверждения.		С практической точки зрения логический язык спецификации свойств программ должен обладать следующими свойствами.	А. Расширяемостью, т.е. возможностью включения в язык новых понятий, определяемых пользователем (программистом). Успех формализации часто зависит от того, насколько удачен выбор понятий, характеризующих искомую проблемную область. Потребности спецификации нельзя покрыть лишь стандартными, универсальными понятиями; поэтому развитый язык спецификации должен быть открыт для последующих расширений пользователями.	Б. Модульностью - использованием средств, расчленяющих сложные спецификации на независимые части (модули) которые позволяют регулировать сложность, накапливать и применять стандартные (встроенные) модули, доступные в пределах одной или нескольких проблемных областей.	В. Иерархичностью структур сложных понятий, допускающих вложенность одних понятий в другие и рассмотрение образуемых иерархий понятий по принципу "сверху вниз". Совместно с модульностью иерархия понятий позволяет достичь ясного и удобного в работе представления спецификаций.	Г. Приближением нотации языка спецификации к естественному языку и используемому языку программирования, что необходимо также для обеспечения ясности спецификации и удобств работы с ними в процессе разработки программ.	Для удовлетворения всем этим требованиям изобразительные средства языка спецификации должны быть более развитые, чем обычные средства языка логики предикатов, создающие для него лишь теоретическую основу. .