Объединяющие теории программирования - Unifying Theories of Programming

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

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

Теории

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

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

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

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

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

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

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

связи

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

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

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

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

${\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, C.A.R .; Цзифэн, Хэ (1 апреля 1998 г.). Объединяющие теории программирования. Отделение колледжа Прентис Холл. п. 320. ISBN  978-0-13-458761-5. Получено 17 сентября 2014.
2. МАШИНА. Hoare, Программирование: Колдовство или наука? Программное обеспечение IEEE, 1 (2): 5–16, апрель 1984 г. ISSN  0740-7459. Дои:10.1109 / MS.1984.234042.
3. Эдсгер В. Дейкстра и Карел С. Шолтен. Исчисление предикатов и семантика программ. Тексты и монографии по информатике. Springer-Verlag New York, Inc., Нью-Йорк, Нью-Йорк, США, 1990. ISBN  0-387-96957-8.

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

• Джим Вудкок и Ана Кавальканти. Учебное введение в дизайн в Unifying Theories of Programming. В Интегрированные формальные методы, том 2999 из Конспект лекций по информатике, страницы 40–66. Springer Берлин / Гейдельберг, 2004. ISBN  978-3-540-21377-2. Дои:10.1007/978-3-540-24756-2_4 CiteSeer^Икс: 10.1.1.99.2929 бумага
• Ана Кавальканти и Джим Вудкок. Учебное введение в CSP в Unifying Theories of Programming. В Методы уточнения в программной инженерии, том 3167 конспектов лекций по информатике, страницы 220–268. Springer Berlin / Heidelberg, 2006. Дои:10.1007/11889229_6 CiteSeer^Икс: 10.1.1.97.3469 бумага

внешняя ссылка

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