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

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

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

Теории

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

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

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

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

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

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

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

Отношения

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

• недекорированные переменные ( ), моделирующие наблюдение за программой в начале ее выполнения; и ${\displaystyle v}$
• начальные переменные ( ), моделирующие наблюдение за программой на более позднем этапе ее выполнения. ${\displaystyle v'}$

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

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

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

• Присвоение значения переменной моделируется как установка и сохранение всех других переменных (обозначаемых ) постоянными: ${\displaystyle E}$ ${\displaystyle a}$ ${\displaystyle a'}$ ${\displaystyle E}$ ${\displaystyle u}$

${\displaystyle a:=E\equiv a'=E\land u'=u}$

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

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

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

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

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

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

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

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

Ссылки

1. Hoare, CAR ; Jifeng, He (1 апреля 1998 г.). Унификация теорий программирования. Prentice Hall. стр. 320. ISBN 978-0-13-458761-5. Получено 17 сентября 2014 г.
2. Хоар, КАР (апрель 1984). «Программирование: колдовство или наука?». IEEE Software . 1 (2): 5–16. doi :10.1109/MS.1984.234042. S2CID  375578.
3. Дейкстра, Эдсгер В .; Шолтен, Карел С. (1990). Исчисление предикатов и семантика программ . Тексты и монографии по информатике. Springer. ISBN 0-387-96957-8.

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

• Вудкок, Джим ; Кавальканти, Ана (2004). "Учебное введение в проекты в унифицированных теориях программирования" (PDF) . Интегрированные формальные методы . Конспект лекций по информатике , страницы. Том 2999. Springer. С. 40–66. doi :10.1007/978-3-540-24756-2_4. ISBN 978-3-540-21377-2.
• Кавальканти, Ана; Вудкок, Джим (2006). "Учебное введение в CSP в унификации теорий программирования" (PDF) . Методы уточнения в программной инженерии . Конспект лекций по информатике. Том 3167. Springer. С. 220–268. doi :10.1007/11889229_6. ISBN 978-3-540-46253-8.

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

• Сайт книги UTP
• Книга UTP на Archive.org