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