Объединение теорий программирования

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

Книга под этим названием, написанная К. А. Хоаром и Хэ Цзифэном, была опубликована в международной серии Prentice Hall по информатике в 1998 году и теперь находится в свободном доступе в Интернете. ^[1]

Теории

Семантической основой UTP является исчисление предикатов первого порядка , дополненное конструкциями с фиксированной точкой из логики второго порядка. Следуя традиции Эрика Хенера , программы являются предикатами в UTP, и на семантическом уровне нет различия между программами и спецификациями. По словам Хоара :

Компьютерная программа идентифицируется самым сильным предикатом, описывающим все соответствующие наблюдения, которые можно сделать о поведении компьютера, выполняющего эту программу. ^[2]

На языке UTP теория — это модель конкретной парадигмы программирования. Теория UTP состоит из трех компонентов:

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

Уточнение программы является важной концепцией в UTP. Программа $P_{1}$ уточняется $P_{2}$ тогда и только тогда, когда каждое наблюдение, которое можно сделать из $P_{2}$ также является наблюдением $P_{1}$ .Определение уточнения является общим для всех теорий UTP:

$P_{1}\sqsubseteq P_{2}\quad {\text{if and only if}}\quad \left[P_{2}\Rightarrow P_{1}\right]$

где $\left[X\right]$ обозначает ^[3] универсальное замыкание всех переменных в алфавите.

Отношения

Самая основная теория UTP — это алфавитное исчисление предикатов, которое не имеет ограничений по алфавиту или условий работоспособности. Теория отношений немного более специализирована, поскольку алфавит отношения может состоять только из:

недекорированные переменные ( $v$ ), моделирование наблюдения за программой в начале ее выполнения; и
штрихованные переменные ( $v'$ ), моделируя наблюдение за программой на более позднем этапе ее выполнения.

Некоторые общеязыковые конструкции можно определить в теории отношений следующим образом:

Оператор пропуска, который никак не изменяет состояние программы, моделируется как реляционная идентичность:

$\mathbf {skip} \equiv v'=v$

Присвоение значения $E$ в переменную $a$ моделируется как установка $a'$ к $E$ и сохраняя все остальные переменные (обозначенные $u$ ) постоянный:

$a:=E\equiv a'=E\land u'=u$

Последовательная композиция двух программ — это просто реляционная композиция промежуточного состояния:

$P_{1};P_{2}\equiv \exists v_{0}\bullet P_{1}[v_{0}/v']\land P_{2}[v_{0}/v]$

Недетерминированный выбор между программами является их наивысшей нижней границей:

$P_{1}\sqcap P_{2}\equiv P_{1}\lor P_{2}$

Условный выбор между программами записывается в инфиксной записи:

$P_{1}\triangleleft C\triangleright P_{2}\equiv (C\land P_{1})\lor (\lnot C\land P_{2})$

Семантика рекурсии определяется наименьшей фиксированной точкой. $\mu \mathbf {F}$ монотонного преобразователя предикатов $\mathbf {F}$ :

$\mu X\bullet \mathbf {F} (X)\equiv \sqcap \left\{X\mid \mathbf {F} (X)\sqsubseteq X\right\}$

Ссылки

^ Хоар, Африка ; Цзифэн, Хэ (1 апреля 1998 г.). Объединение теорий программирования . Прентис Холл. п. 320. ИСБН 978-0-13-458761-5 . Проверено 17 сентября 2014 г.
^ Хоар, ЦАР (апрель 1984 г.). «Программирование: волшебство или наука?». Программное обеспечение IEEE . 1 (2): 5–16. дои : 10.1109/MS.1984.234042 . S2CID 375578 .
^ Дейкстра, Эдсгер В .; Схолтен, Карел С. (1990). Исчисление предикатов и семантика программ . Тексты и монографии по информатике. Спрингер. ISBN 0-387-96957-8 .

Дальнейшее чтение

Вудкок, Джим ; Кавальканти, Ана (2004). «Введение в дизайн в Unifying Theory of Programming» (PDF) . Интегрированные формальные методы . Конспекты лекций по информатике , стр. Том. 2999. Спрингер. стр. 40–66. дои : 10.1007/978-3-540-24756-2_4 . ISBN 978-3-540-21377-2 .
Кавальканти, Ана; Вудкок, Джим (2006). «Введение в CSP в унификации теорий программирования» (PDF) . Методы совершенствования в программной инженерии . Конспекты лекций по информатике. Том. 3167. Спрингер. стр. 220–268. дои : 10.1007/11889229_6 . ISBN 978-3-540-46253-8 .

Внешние ссылки

[1] Хоар, Африка ; Цзифэн, Хэ (1 апреля 1998 г.). Объединение теорий программирования . Прентис Холл. п. 320. ИСБН 978-0-13-458761-5 . Проверено 17 сентября 2014 г.

[2] Хоар, ЦАР (апрель 1984 г.). «Программирование: волшебство или наука?». Программное обеспечение IEEE . 1 (2): 5–16. дои : 10.1109/MS.1984.234042 . S2CID 375578 .

[3] Дейкстра, Эдсгер В .; Схолтен, Карел С. (1990). Исчисление предикатов и семантика программ . Тексты и монографии по информатике. Спрингер. ISBN 0-387-96957-8 .

[1]

[2]

[3]