WikiDer > Объединяющие теории программирования - Википедия

Объединяющие теории программирования (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 {тогда и только тогда, когда}} quad left [P_ {2} Rightarrow P_ {1} right]}$

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

связи

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

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

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

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

${ Displaystyle mathbf {пропустить} Equiv v '= v}$

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

${ Displaystyle а: = Е эквив а '= Е земля и' = и}$

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

${ 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} Trianglerleft C triangleright P_ {2} Equiv (C land P_ {1}) lor ( lnot C land P_ {2})}$

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

${ Displaystyle му Икс пуля mathbf {F} (X) Equiv sqcap left {X mid mathbf {F} (X) sqsubseteq X right }}$

Рекомендации

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

• Джим Вудкок и Ана Кавальканти. Учебное введение в дизайн в 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