Новосибирский государственный университет

Факультет информационных технологий

В. И. ШЕЛЕХОВ

Предикатное программирование

Учебное пособие

Новосибирск

УДК 004.432.42

ББК 22.183.492

Ш 427

Шелехов В. И. Предикатное программирование: Учеб. пособие / Новосиб. гос. ун-т. Новосибирск, 2009. 109 с.

ISBN 978-5-94356-878-7

Предназначено для студентов факультета информационных технологий и механико-математического факультета, а также всех желающих изучить формальные методы корректности программ и построения эффективных программ в парадигме предикатного программирования. Пособие включает содержание первого семестра курса «Предикатного программирование».

Издание подготовлено в рамках реализации Программы развития государственного образовательного учреждения высшего профессионального образования «Новосибирский государственный университет» на 2009–2018 годы.

© Новосибирский государственный университет, 2009

ISBN 978-5-94356-878-7 © В. И. Шелехов, 2009

Оглавление

Введение в курс предикатного программирования.............................................................. 5

1. Общее понятие программы........................................................................................... 6

1.1. Автоматическая вычислимость....................................................................................... 6

1.2. Спецификация программы.............................................................................................. 7

1.3. Формы спецификации программы.................................................................................. 9

Список литературы................................................................................................................. 10

2. Корректность программ с предикатной спецификацией................................... 12

2.1. Предикатная спецификация программы...................................................................... 12

2.2. Логическая семантика языка программирования....................................................... 13

2.3. Модель корректности программы................................................................................ 15

2.4. Система правил доказательства корректности операторов........................................ 16

2.4.1. Правила для корректного оператора.................................................................. 17

2.4.2. Правила корректности для параллельного оператора...................................... 17

2.4.3. Правила корректности для оператора суперпозиции....................................... 17

2.4.4. Правила корректности для условного оператора.............................................. 18

2.5. Система правил вывода программы из спецификации............................................... 19

2.5.1. Однозначность предикатов................................................................................. 19

2.5.2. Теорема тождества спецификации и программы.............................................. 19

2.5.3. Правила корректности для параллельного оператора...................................... 20

2.5.4. Правила корректности для оператора суперпозиции....................................... 21

2.5.5. Правила корректности для условного оператора.............................................. 22

2.6. Заключение.............................................................................................................. 22

Список литературы................................................................................................................. 23

3. Математические основы........................................................................................... 24

3.1. Отношения порядка....................................................................................................... 24

3.2. Наименьшая неподвижная точка.................................................................................. 25

3.3. Математическая индукция............................................................................................ 25

Список литературы................................................................................................................. 26