Формализация КЯ

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

Денотационный подход состоит в определении семантики языка путем подстановки каждому выражению соответствующего элемента из множества денотатов в функции <р интерпретации символов сигнатуры языка. Каждым константе с е С, функциональному символу f eF и предикатному символу реР сопоставляется объект из множества денотат. Этот способ интерпретации семантики выражений и операторов языка аналогичен денотационной семантике ЯП. Главное отличие семантики КЯ от семантики программ — ее неконструктивность. С каждым КЯ можно связать некоторую дедуктивную теорию, которая отражает свойства концепторов.

Формальная дедуктивная теория строится путем выделения из множества всех формул подмножества аксиом и правил вывода. Для каждой пары R^,R2 формул дедуктивной теории и каждого оператора I создается операторная формула {R{}I{R2} с утверждением: если R истинно перед выполнением оператора /, то завершение оператора I обеспечивает истинность R2, т.е. формула R{ — предусловие, a R2 постусловие оператора I. С помощью неконструктивных объектов и неразрешимых формул этой теории можно адекватно описывать свойства неэффективных процедур.

Аксиоматическое описание КЯ — это аксиомы и утверждения относительно концепторного описания и проведения дедуктивного доказательства и верификации этого описания.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >