Семантическая теория программ

1.

Семантическая
теория
программ

2.

ОПИСАНИЕ СМЫСЛА ПРОГРАММЫ
• Программа – описание алгоритма и данных на
некотором языке программирования для
выполнения на компьютере.
• 1 программе соответствует 1 алгоритм,
представляющий функцию, вычисляемую
программой.
• Функция, вычисляемая программой –
однозначное отображение входных данных на
множество выходных данных.
• Семантика – описание смысла программы

3.

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

4.

ОПИСАНИЕ СМЫСЛА ПРОГРАММЫ
• Алфавит языка программирования – множество
букв, цифр и специальных символов (знаков
операций, разделителей, специальных ключевых
слов).
Основные объекты языка программирования
• Информационные структуры (данные)
• Управляющие структуры (вычисления)
• Контролирующие структуры
• Тип данных – множество значений и набор
операций, выполняемых над этими значениями
или вырабатывающие эти значения как результат

5.

ОПИСАНИЕ СМЫСЛА ПРОГРАММЫ

6.

ОПИСАНИЕ СМЫСЛА ПРОГРАММЫ
Типы данных:
• Простые типы данных (bool, char, integer и т.д.)
• Составные типы данных (массив, структура,
файл)
Операционные управляющие структуры:
• Простые операторы (операторы присваивания,
ввода, вывода)
• Составные операторы (if-then, if-then-else, dowhile, case)

7.

СЕМАНТИКА
Семантика
• Операционная семантика
• Аксиоматическая семантика
• Денотационная семантика
• Декларативная семантика

8.

ОПЕРАЦИОННАЯ СЕМАНТИКА
• Операционная семантика – описание смысла
программы посредством выполнения ее
операторов на реальной или виртуальной
машине.
Трудности:
• сложность и индивидуальные особенности
аппаратного обеспечения компьютера и
операционной системы затрудняют понимание
происходящих действий.
• выполненное таким образом семантическое
определение будет доступно только для людей с
абсолютно идентичной конфигурацией
компьютера.

9.

Семантика конструкции
for языка СИ

10.

Пример
низкоуровневого языка

11.

Пример
низкоуровневого языка

12.

ОПЕРАЦИОННАЯ СЕМАНТИКА
Описание операционной семантики функций
Подстановка <s, E, t> терма в выражение E - переписывание
выражения E с заменой каждого вхождения в него символа s на
выражение t .
Множество правил подстановок:
<x1, x2, ..., xk; fi(t1, t2, ... , tk) → Ei; t1, t2, ... , tk >,
где t1, t2, ...,tk – конкретные аргументы (значения или определяющие
их выражения) данной функции.

13.

ОПЕРАЦИОННАЯ СЕМАНТИКА
Интерпретация равенств :
1. Заданы входные данные d1,…,dn
2. Подстановка данных в выражения, определяемых в Ei, где
это возможно
3. Просматриваются правые части полученных равенств.
1.
2.
3.
Если правая часть является каким-либо значением, то оно и
будет значением функции, указанной в левой части этого
равенства.
Если правая часть не является каким-либо значением, то правая
часть является выражением, содержащим вхождения каких-либо
определяемых функций с теми или иными наборами
аргументов
Если для такого вхождения функция с данным набором
аргументов есть в левой части одного из равенств, подставляется
ее вычисленное значение, иначе формируется новое равенство.

14.

ПРИМЕР
FACT(0)=1,
FACT(n)=n*FACT(n-1).
3!

15.

АКСИОМАТИЧЕСКАЯ
СЕМАНТИКА
• Программа рассматривается как функция,
преобразующая начальное состояние памяти в
конечное.
• Свойства операторов языка выражаются в виде логических формул, устанавливающих отношения
между переменными программы. В этом случае
явно описываются свойства состояний памяти, а не
сами состояния.
• Формальная семантика языка программирования
состоит в том, что формулируются некоторые
утверждения о свойствах конструкций языка, из которых можно вывести утверждения о свойствах
конкретной программы

16.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
Семантику каждой синтаксической конструкции языка можно определить как некий набор аксиом
или правил вывода, который можно использовать для вывода результатов выполнения этой
конструкции.
Чтобы понять смысл всей программы, эти аксиомы и правила вывода следует использовать так же,
как при доказательстве обычных математических теорем. В предположении, что значения входных
переменных удовлетворяют некоторым ограничениям, аксиомы и правила вывода могут быть
использованы для получения (вывода) ограничений на значения других переменных после
выполнения каждого оператора программы.
В конце концов, когда программа выполнена, мы получаем доказательство того, что вычисленные
результаты удовлетворяют необходимым ограничениям на их значения относительно входных
значений. То есть, доказано, что выходные данные представляют значения соответствующей
функции, вычисленной по значениям входных данных.
Высказывание – предикат помещенный в программу. Высказывание, непосредственно
предшествующее оператору программы, описывает ограничения, наложенные на переменные в
данном месте программы. Высказывание, следующее непосредственно за оператором
программы, описывает новые ограничения на те же (а возможно, и другие) переменные после
выполнения оператора.
Операции
Конъюнкция b AND c
Дизъюнкция b OR c
Отрицание NOT b
Импликация b
c
Равенство b=c

17.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
• Правила построения высказываний:
o F и Т – высказывания.
o Идентификаторы являются высказываниями.
o Если b – высказывание, то и (NOT b) высказывание.
o Если b и с – высказывания, то (b OR с), (b AND с), (b = с),
(b с) – также высказывания
• Таблица истинности

18.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
• Состояние s – это функция из множества
идентификаторов в множество значений F и Т.
• Высказывание E определено в состоянии s, если
каждый идентификатор из E встречается в s.
• s(E) – значение E в состоянии s – получаемое
заменой всех вхождений идентификаторов b в
высказывание E на их значения s(b) и
вычислением получившегося постоянного
высказывания.
• Тавтология – высказывание, истинное в любом
состоянии, в котором оно определено.

19.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
Правила старшинства операций
• Одноименные операции выполняются
последовательно слева направо.
• Порядок вычислений различных между собой и
смежных в записи высказывания операций
определяется списком: NOT, AND, OR, , =.
• Высказывания Е1 и Е2 эквивалентны, если и только
если Е1 = Е2 есть тавтология. Здесь Е1~Е2 –
эквивалентность.

20.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
Законы коммутативности: (Е1®Е2) = (Е2® Е1),
®– обозначает операции = , AND, OR.
Законы ассоциативности:
(Е1® Е2) ® Е3 = Е1 ® (Е2®Е3),
®– обозначает операции AND, OR.
Законы дистрибутивности: (Е1 ® Е2) © Е3 = (Е1 ® E3) ©(Е2 ® Е3),
© и ®– обозначают операции AND, OR.
4. Законы де Моргана:
NOT (Е1 © Е2) = NOT Е1® NOT Е1),
© и ® – обозначают операции AND, OR.
Закон отрицания: NOT (NOT Е1) = Е1.
Закон исключенного третьего: Е1 OR NOT Е1 = Т.
Закон противоречия: Е1 AND NOT Е1 = F.
Закон импликации: (Е1 Е2) = NOT Е1 OR Е2.
Закон равенства: (Е1 = Е2) = (Е1 Е2) AND (Е2 Е1).
Законы упрощения OR:
Е1 OR Е1 = Е1, Е1 OR (Е1 AND Е2) = Е1, Е1 OR Т = Т, Е1 OR F = Е1.
Законы упрощения AND:
Е1 AND Е1 = Е1, Е1 AND (Е1 OR Е2) = Е1, Е1 AND Т = Е1, Е1 AND F =
F.
Закон тождества Е1 = Е1.

21.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
• Правило постановки:
Если е1 = е2 – эквивалентность, а Е(х) – высказывание,
записанное как функция от одного из своих
идентификаторов х, тогда
Е(е1) = Е(е2) и Е(е2) = Е(е1) – эквивалентности.
• Правило транзитивности:
Если е1 = е2 и е2 = е3 – эквивалентности,
то е1 = е3 – эквивалентность.
• Для формулирования развернутых высказываний
используются кванторы

22.

Аксиоматическая семантика
Опишем решаемую задачу или функцию, которую должна выполнять
программа, т.е. специфицируем свойства программы.
Эту функцию f надо задать так, чтобы было видно, к каким значениям
применима функция и к какой области относятся ее результаты.
Обозначим область определения f через D, а область значений - через
R. Поскольку функция f задает отображение f: D→R, она представляет
собой некоторое подмножество (отношение) f ċ [D×R].
Логическая спецификация определяет f в виде:
pre-f(d), d€D - предусловие функции f, характеризующее множество
элементов области D;
post-f(d, r), d€D, r€R - постусловие функции f, характеризующее связь
между d€D и r€R.
Формальный смысл этих предикатов устанавливается их взаимосвязью
следующей формулой:
Для любого d(pre-f(d)→post-f(d, f(d))) ( для всех d€D истинность
предусловия влечет истинность постусловия.
При программной реализации Pg функции f на компьютере
абстрактные множества D и R интерпретируются на множестве State
состояний памяти. При этом каждое состояние памяти характеризуется
множеством значений переменных программы Pg, включая и
неопределенные.

23.

Логическая спецификация программы Pg,
описывающая ее функционирование, может быть
определена на множестве состояний памяти
предикатами:

24.

Инвариант точки q
• Предикаты pre-Pg и post-Pg, характеризуют только
вход и выход программы. Для более полной
логической спецификации свойств программы
обычно требуется характеризовать ее поведение в
некоторых промежуточных, точках. Для этой цели
используют так называемые инварианты.
• Определение Инвариантом точки q программы
называют формулу φq(x1, x2,…, xm) логического языка
спецификации, такую, что φq истинно для набора
значений x1, x2,…, xm программных переменных при
каждом прохождении выполнения через точку q.

25.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
Триада Хоара
{P} S {Q}
P – предусловия, S – программа, Q – постусловия.
Смысл тройки Хоара: если Р истинно перед выполнением
оператора А и выполнение оператора А завершается, то Q
истинно для значений переменных, соответствующих завершению
А. Формально тройка Хоара представляется предикатом:
{P}A{Q}: st(P(st) Ù fin(A, st)→Q(st, fA(st))),
вычисляемая оператором А.
где fA - функция,

26.

Аксиоматическая семантика
Пример Рассмотрим оператор присваивания для
целочисленных переменных и постусловие:
sum := 2 * х + 1 {sum > 1}
Одним из возможных предусловий данного
оператора может быть {х > 10}.

27.

Аксиоматическая семантика
Тройка Хоара является утверждением об операторе и
представляет собой элементарную единицу рассуждений о
свойствах программы в аксиоматической теории. Она
формально описывает семантику оператора.
Всю программу можно рассматривать как один сложный
оператор и связать с ней тройку Хоара. Тогда доказательство
частичной корректности программы сводится к доказательству
истинности ее тройки Хоара.

28.

Аксиоматическая семантика
Важным общезначимым свойством тройки Хоара является
возможность изменения предусловия или постусловия
фиксированного оператора А с сохранением истинности его
тройки. Соответствующие правила изменения (усиления и
ослабления) установлены законами логического следствия
(консеквенции):
Первый закон утверждает, что, если выполнение оператора А
обеспечивает истинность постусловия R, то оно также обеспечивает
истинность каждого постусловия Q, которое следует из R. Второй
закон утверждает, что если R известное предусловие оператора А,
приводящего к постусловию Q, то это же относится к любому
другому утверждению Р, которое влечет R.

29.

Аксиоматическая семантика
Говорят, что Q в первом из рассматриваемых законов
является ослаблением R, а Р во втором - усилением R.
Законы консеквенции утверждают, что для любого
оператора А можно произвольным образом ослаблять (вплоть до
true) постусловие и произвольным образом усиливать (вплоть
до false) предусловие. При этом истинное значение тройки Хоара
сохраняется. Отсюда следует неизменная истинность троек
Хоара вида:
{P}A{t} и {f}A{Q}.

30.

Аксиоматическая семантика
Определения троек Хоара для простых операторов играют роль
аксиом, а для композиций операторов устанавливаются правила
вывода, выражающие свойства композиции через свойства ее
составных частей.

31.

Аксиоматическая семантика

32.

Аксиоматическая
семантика
Семантика сложных операторов описывается правилами
вывода, показывающими, как свойства составной конструкции
связаны со свойствами ее частей. Каждое правило содержит
одну посылку или несколько и единственное следствие (тройку
Хоара для рассматриваемого сложного оператора).
Семантика составного оператора характеризуется тем, что
свойства в неизменной форме могут переноситься из
постусловия одного оператора последовательности в
предусловие следующего за ним оператора. Правило вывода
для последовательности операторов формулируется так: из
истинности троек Хоара операторов последовательности
выводится (следует) истинность тройки Хоара
последовательности операторов.
Любую последовательность операторов можно рассматривать
как последовательность двух операторов. Правило вывода для
последовательности двух операторов имеет вид:
{Р} A1 {V), {V} А2 {Q} |- {Р} А1; А2 {Q}.

33.

Аксиоматическая
семантика
Если требуется установить истинность спецификации условного
оператора if В then А1 else А2, то необходимо доказать два
утверждения относительно истинности спецификаций
альтернативных операторов:

34.

Аксиоматическая
семантика
Истинность тройки Хоара для оператора цикла while В do A
выводится из истинности тройки Хоара для его тела А. При этом
истинность тройки для А должна сохраняться при каждом
выполнении А. Из этих соображений и схемы цикла строим
правило вывода:

35.

Аксиоматическая
семантика
Тройка Хоара оператора repeat A until В

36.

АКСИОМАТИЧЕСКАЯ СЕМАНТИКА
• Сильнейшее постусловие программы (strongest
postcondition) sp(S,R) - это предикат,
определяющий все те состояния программы S, в
которые преобразуются по завершении S все
состояния, удовлетворявшие предикату R до
старта S
• Слабейшими предусловиями (weakest
precondition) называются наименьшие
предусловия R, обеспечивающие выполнение
соответствующего постусловия Q: (wp(S,R)).

37.

ПРИМЕР
• После завершения программы
S значение х возрастет на 3.
Поэтому, если R: х > z+5 до
выполнения S: х:=х+3,
то sp(S, I): х > z+8
• После завершения программы
S значение х возрастет на 3.
Поэтому, если Q: y > 5 после
выполнения S: х:=х+3,
то wp(S, I): х > 2

38.

Слабейшее предусловие
Если для каждой конструкции (оператора) языка по заданным
постусловиям можно вычислить слабейшее предусловие, то
можно построить доказательство для программы, написанной
на данном языке.
Доказательство начинается с использования результатов,
которые надо получить после выполнении программы. Иначе
говоря, используются результаты, являющиеся постусловиями
последней конструкции (оператора) программы.
Процесс доказательства идет от конца программы к ее началу
с последовательным вычислением слабейших предусловий для
каждой конструкции (оператора).
В начале программы ее первое слабейшее предусловие
отражает условия, при которых программа сможет прийти к
требуемым результатам.

39.

СВОЙСТВА wp(S,R)
Определение семантики оператора S дается в виде правила,
описывающего, как для любого заданного постусловия R можно вывести
слабейшее предусловие wp(S,R).
Cвойства (по Э. Дейкстре) wp(S, R):
• wp(S, F) = F для любого S (закон исключенного
чуда).
• Закон монотонности. Для любого S, предикатов P
и R таких, что P => R для всех состояний,
справедливо для всех состояний wp(S, P) => wp(S,
R).
• Дистрибутивность конъюнкции. Для любых S, P, R
справедливо
wp(S, P) AND wp(S, R) = wp(S, P AND R).
• Дистрибутивность дизъюнкции. Для любых S, P, R
справедливо wp(S, P) OR wp(S, R) = wp(S, P OR R).

40.

АКСИОМАТИЧЕСКОЕ ОПРЕДЕЛЕНИЕ
ОПЕРАТОРОВ
• Оператор присваивания
x := E, x – простая переменная, E – выражение.
Y>5 |x+3>5 |x>2

41.

АКСИОМАТИЧЕСКОЕ ОПРЕДЕЛЕНИЕ
ОПЕРАТОРОВ
• Составной оператор
begin S1; S2; ... ; Sn end .
Определим слабейшее
предусловие для
последовательности двух
операторов:

42.

АКСИОМАТИЧЕСКОЕ ОПРЕДЕЛЕНИЕ
ОПЕРАТОРОВ
• Оператор выбора
if B1 → S1 П B2 → S2 ... П Bn → Sn fi.
n≥ 0, B1, B2, ..., Bn – логические выражения, охрана;
S1, S2, ..., Sn – операторы;
пара Bi → Si - охраняемая команда;
П – разделитель;
if и fi играют роль операторных скобок.
Выбирается одна из охраняемых команд Bi → Si, у
которой значение Bi «истина», и выполняется Si.
Определим слабейшее предусловие:
wp(if, R) = BB AND (B1 => wp(S1, R)) AND ... AND (Bn
=> wp(Sn, R)), где BB = B1 OR B2 OR ... OR Bn.

43.

Оператор выбора

44.

АКСИОМАТИЧЕСКОЕ ОПРЕДЕЛЕНИЕ
ОПЕРАТОРОВ
Оператор цикла. do B → S od.
Обозначим это соотношение через DO и представим
его в следующем виде:
DO: do B1 → S1 П B2 → S2 ... П Bn → Sn od,
где n≥0, Bi → Si – охраняемые команды.
Выполняется оператор следующим образом. Пока
возможно, выбирается охрана Bi со значением истина, и
выполняется соответствующий оператор Si. Как только
все охраны будут иметь значение ложь, выполнение DO
завершится.
Выбор охраны со значением истина и выполнение
соответствующего оператора называется выполнением
шага цикла. Если истинными являются несколько охран,
то выбирается любая из них.
оператор DO эквивалентен оператору
do BB → if B2 → S1 П B2 → S2 ... П Bn → Sn fi od или do BB →
IF od, где BB – дизъюнкция охран, IF – оператор выбора.

45.

Пример аксиоматического описания оператора
цикла для алгоритма Евклида

46.

ИНВАРИАНТ ЦИКЛА
Инвариант цикла — это утверждение, истинное
перед циклом и после каждого прохода тела
цикла.
Доказательство правильности написания цикла:
• Инвариант истинен до начала выполнения цикла.
• Инвариант сохраняет свою истинность после
выполнения тела цикла при истинности условия
продолжения цикла.
• Из истинности инварианта и условия завершения
цикла (отрицания условия продолжения цикла)
следует корректность результата.

47.

ИНВАРИАНТ ЦИКЛА
Инвариантом называется логическое выражение, истинное перед
началом выполнения цикла и после каждого прохода тела цикла,
зависящее от переменных, изменяющихся в теле цикла.
Стандартный программный контекст суммирования основан на цикле,
имеющем соответствующий инвариант:
В контексте суммирования выражение в теле цикла s=s+A[i] сохраняет
свойство переменной s быть суммой элементов массива он нулевого до
текущего. Смысл переменной s в правой и левой части различен. В правой
части находится «старое» значение суммы для предыдущего шага,
т.е. s=A[0]+A[1]+…+A[i-1], в левой части – уже для текущего.
На первом шаге начальное значение суммы обнуляется.
Аналогичный порядок рассуждений применим и для контекста,
обеспечивающего нахождение максимума (минимума):
Выражение if (A[i]>s) s=A[i]; сохраняет свойство переменной s быть
максимальным значением элементов массива от 0 до i-го.
Действительно, если в операции сравнения переменная s содержит
максимальное значение в диапазоне от 0 до i-1, то выражение в целом
определяет максимальное значение с учетом текущего шага: максимум
изменяется, если текущее значение A[i] превышает старое значение
максимума, иначе – ничего не происходит.

48.

ИНВАРИАНТ ЦИКЛА
Требуется найти наибольший общий делитель d двух
целых чисел n и m: d =НОД(n, m).
Инвариант цикла для нахождения НОД(n, m) : пусть имеется пара
чисел a и b таких, что НОД(a, b) = НОД(n, m). На каждом шаге
цикла будем переходить к другой паре чисел a и b таких, что
НОД(a, b) = НОД(n, m). И так будем продолжать до тех пор, пока
значение НОД не станет очевидным. Таким образом, инвариант
цикла сформулируем так:
НОД(a, b) = НОД(n, m).
Если d =НОД(n, m), то это же значение d является и НОД(m, r), где
r – остаток от деления n на m, то есть НОД(n, m) = НОД(m, r).
Например: НОД(126, 12) = НОД(12, 6) = НОД(6, 0) = 6

49.

ИНВАРИАНТ ЦИКЛА
Алгоритм решения задачи можно представить так:
Начальная инициализация: пусть a = n, b = m. Очевидно, что НОД(a, b) = НОД(n, m).
Находим r и делаем a = b и b = r. При этом выражение НОД(a, b) = НОД(n, m) остается
справедливым.
Как только b станет равно 0, тогда НОД(a, 0) = НОД(n, m) = a.
Программа, реализующая этот алгоритм:
int r, a = n, b = m;
// Инвариант: НОД(a, b) = НОД(n, m)
// Цикл заканчивается при b = 0, тогда НОД (a, 0) = a
while (b)
{
// Инвариант: НОД(a, b) = НОД(n, m) выполняется
r = a % b;
a = b;
b = r;
// Инвариант: НОД(a, b) = НОД(n, m) выполняется
}
// Инвариант: НОД(a, b) = НОД(n, m) выполняется
cout << “НОД (“ << n << “, ” << m << “) = ” << a << endl;

50.

ИНВАРИАНТ ЦИКЛА

51.

ИНВАРИАНТ ЦИКЛА

52.

Денотационная
семантика
• Языковая конструкция “Двоичные числа”:
• <двоичное_число> ::= 0 | 1 | <двоичное_число> 0 |
<двоичное_число> 1
• Пусть область определения семантических значений
объектов представляет собой множество неотрицательных
десятичных целых чисел N. Это те объекты, которые будем
связывать с двоичными числами.
• Семантическая функция Мb отображает синтаксические
объекты в объекты множества N согласно указанным выше
правилам. Сама функция Мb определяется следующим
образом:
• Мb('0') = 0, Мb('1')=1
• Мb(<двоичное_число> '0') = 2*Мb(<двоичное_число>)
• Мb(<двоичное_число> '1') = 2*Мb(<двоичное_число>) + 1

53.

Денотационная
семантика

54.

Денотационная
семантика
Пусть состояние s программы определяется набором упорядоченных
пар
{<i1, v1>, <i2, v2>, …, <in, vn>}.
Каждый параметр i является именем переменной,а соответствующие
параметры v являются текущими значениями данных переменных.
Любой из параметров v может иметь специальное значение undef, ука
зывающее, что связанная с ним величина в данный момент не
определена.
Пусть VARMAP - функция двух параметров: имени переменной и
состояния программы. Значение функции VARMAP(ik, s) равно vk.
Большинство семантических функций отображения для программ и
программных конструкций отображают состояния в состояния.
Эти изменения состояний используются для определения смысла
программ и программных конструкций. Такие языковые конструкции,
как выражения, отображаются не в состояния, а в величины.

55.

Денотационная семантика
Простые выражения (описание БНФ)
Функция отображения для выражения E и состояния s

56.

Денотационная
семантика
Оператор присваивания
Оператор присваивания можно представить как вычисление выражения
плюс присваивание его значения переменной, находящейся в левой
части.

57.

СЕМАНТИКИ
• Декларативная семантика - характеристика
языков логического программирования, в
которых программы состоят из объявлений
(деклараций), а не из операторов присваивания
и управляющих операторов. Эти объявления в
действительности являются операторами, или
высказываниями, в символьной логике.