Семантика языков программирования

Сентябрь 7, 2022

Главная
Алгебра
Семантика языков программирования

Содержание

2. Зачем нужна формальная семантика? Чтобы точно знать возможности языка программирования. Чтобы доказывать корректность программы, а не
3. Эквивалентные преобразования программы Зная, что if true then C1 else C2 делает тоже самое, что и
4. Эквивалентны ли фрагменты программы? begin C1 ; if B then C2 else C3 end if B
5. А эти? begin if B then C2 else C3 ; C1 end if B then begin
6. Синтаксические категории е ∈ Exp op ∈ Op n ∈ Num Определения op ::= + |
7. Методы определения семантики Конкретная операционная семантика Естественная семантика Вычислительная (структурно – операционная) семантика Денотационная семантика
8. Конкретнтая операционная семантика языка Exp topostfix(N,S,[N|S]) :- number(N). topostfix(E,S,R) :- E =.. [Op,A,B], member(Op,[+,-,*,/]), topostfix(A,[Op|S],S1), topostfix(B,S1,R).
9. Естественная семантика Это аксиоматическая система, определяющая смысл каждой конструкции языка в виде вычисляемого ею значения. Определим
10. Правила, определяющие естественную семантику языка арифметических выражений Правило CR Правило OpR n ⇒ n e ⇒
11. Пусть нужно вычислить значение выражения 3 * 4 + 8 div (4 – 2). Это сумма,
12. В конце концов, получив численную константу применим правила CR: Вычисление значения арифметических выражений (продолжение) 3 ⇒
13. Реализация естественной семантики языка Exp eval(N,N) :- number(N). eval(E,R) :- E =.. [Op,E1,E2], member(Op,[+,-,*,/]), eval(E1,R1), eval(E2,R2),
14. Индукция Свойства семантики языка программирования можно доказывать по индукции. Метод математической индукции: Чтобы доказать свойство P(x)
15. Пример Пусть нужно доказать, что сумма первых n натуральных чисел равна n * (n+1) div 2,
16. Структурная индукция Метод математической индукции применим к натуральным числам потому, что их множество определяется по индукции:
17. Закон « map после (++)» Для всех списков xs, ys и функций f выполняется равенство: map
19. Теорема. Отношение ⇒ для языка Exp является функцией Для всех выражений е ∈ Exp справедливо, что
20. Первый случай Если n ⇒ v, а для вычисления v мы могли использовать только правило CR
22. Скачать презентацию

Слайд 2

Зачем нужна формальная семантика?
Чтобы точно знать возможности языка программирования.
Чтобы доказывать

корректность программы, а не экспериментировать с компилятором.
Чтобы убедиться, что компилятор работает корректно.
Для облегчения переносимости компилятора на различные платформы.

Слайд 3

Эквивалентные преобразования программы
Зная, что if true then C1 else C2 делает тоже

самое, что и C1 можно упростить программу.
Используя формальную семантику можно доказывать эквивалентность и более сложных фрагментов программы.

Слайд 4

Эквивалентны ли фрагменты программы?
begin
C1 ; if B
then C2

else C3
end

if B
then
begin
C1 ; C2
end
else
begin
C1 ; C3
end

Слайд 5

А эти?
begin
if B
then C2
else C3 ;
C1
end
if

B
then
begin
C2 ; C1
end
else
begin
C3 ; C1
end

Слайд 6

Синтаксические категории е ∈ Exp op ∈ Op n ∈ Num
Определения op ::= + | - | * | div e ::= n |

e/ op e//

Абстрактный синтаксис языка арифметических выражений

Типичные предста -вители

Синтакси -ческие категории

Слайд 7

Методы определения семантики
Конкретная операционная семантика
Естественная семантика
Вычислительная (структурно – операционная) семантика
Денотационная семантика

Слайд 8

Конкретнтая операционная семантика языка Exp
topostfix(N,S,[N|S]) :- number(N).
topostfix(E,S,R) :-
E =..

Слайд 9

Естественная семантика
Это аксиоматическая система, определяющая смысл каждой конструкции языка в виде

вычисляемого ею значения.
Определим семантику языка арифметических выражений.
Для этого понадобится отношение
⇒ : Exp → Num ,
отображающее множество арифметических выражений на множество чисел.
Оно определяется индуктивно:
Правило 1: Для каждой числовой константы n, n ⇒ n.
Правило 2: Если e ⇒ v и e’ ⇒ v’, то e op e’ ⇒ Ap (op, v, v’).

Слайд 10

Правила, определяющие естественную семантику языка арифметических выражений
Правило CR
Правило OpR
n ⇒ n
e ⇒

e’⇒ v’

e op e’ ⇒ Ap(op, v, v’)

Слайд 11

Пусть нужно вычислить значение выражения
3 * 4 + 8 div (4

– 2).
Это сумма, и применение правила OpR приведёт к
Для вычисления применим ещё два раза правила OpR:

Вычисление значений арифметических выражений

3 * 4 ⇒ v

8 div (4 – 2) ⇒ v’

3 * 4 + 8 div (4 – 2) ⇒ Ap(+NUM, v, v’)

3 ⇒ v’

4 ⇒ v”

3 * 4 ⇒ Ap(*NUM, v’, v”)

8 ⇒ v’

(4 – 2) ⇒ v”

8 div (4 – 2) ⇒ Ap(/NUM, v’, v”)

Слайд 12

В конце концов, получив численную константу применим правила CR:
Вычисление значения арифметических

выражений (продолжение)

3 ⇒ 3

4 ⇒ 4

8 ⇒ 8

2 ⇒ 2

Выполнив подстановку значений промежуточным переменным, получим окончательный результат.
Рассмотренная нами процедура поиска результата напоминает нам работу пролог - машины, только мы не фиксировали порядок применения правил.

Слайд 13

Реализация естественной семантики языка Exp
eval(N,N) :- number(N).
eval(E,R) :-
E =.. [Op,E1,E2],

member(Op,[+,-,*,/]),
eval(E1,R1),
eval(E2,R2),
Ee =.. [Op,R1,R2],
R is Ee.
test(V) :-
eval(2*3+4-6/2, V).

Слайд 14

Индукция
Свойства семантики языка программирования можно доказывать по индукции.
Метод математической индукции: Чтобы доказать

свойство P(x) всех натуральных чисел, нужно доказать два отдельных утверждения: 1) Истинность P(0). Это база индукции. 2) То, что из истинности P(k) следует истинность P(k+1) . Это индуктивный шаг.
Почему? - Потому, что эти два утверждения определяют рекурсивный процесс, который проверит истинность свойства P(x) для всех натуральных чисел.

Слайд 15

Пример
Пусть нужно доказать, что сумма первых n натуральных чисел равна n *

(n+1) div 2, то есть 0 + 1 + … + n = n * (n+1) div 2.
Это свойство всех натуральных чисел.
Итак, для доказательства P(n), для всех n ∈ Ν нужно показать, что: 1) 0 = 0 * (0+1) div 2. Для этого достаточно просто выполнить арифметические действия. 2) Из истинности (1) 0 + 1 + … + n = n * (n+1) div 2 вывести (2) 0 + 1 + … + n + (n+1) = (n+1) * (n+2) div 2. Прибавим к обоим частям истинного равенства (1) (n+1) получим: 0 + 1 + … + n + (n+1) = n * (n+1) div 2 + (n+1). Далее выполнив преобразование правой части получим: n * (n+1) div 2 + (n+1) = {умножим и поделим (n+1) на 2 } n * (n+1) div 2 + 2 * (n+1) div 2 = {сложим дроби} (n * (n+1) + 2 * (n+1)) div 2 = {вынесем (n+1)за скобку} (n+1) * (n+2) div 2.

Слайд 16

Структурная индукция
Метод математической индукции применим к натуральным числам потому, что их

множество определяется по индукции:
0 ∈ Ν
Если n ∈ Ν, то и n+1 ∈ Ν.
Доказательство по индукции можно строить и для других множеств, заданных по индукции. Например, возьмем множество списков натуральных чисел. Обозначим через [] – пустой список, а через : - операцию построения списка из головы и хвоста. Наше множество Lists(Ν) можно определить так.
[] ∈ Lists(Ν)
Если l ∈ Lists(Ν), а n ∈ Ν, то n:l ∈ Lists(Ν) .
В форме правил:

[] ∈ Lists(Ν)

l ∈ Lists(Ν)

n ∈ Ν

n:l ∈ Lists(Ν)

Слайд 17

Закон « map после (++)»
Для всех списков xs, ys и функций

f выполняется равенство:
map f (xs++ys) = map f xs ++ map f ys ,
при условии что правильно определены типы.

Слайд 18

Слайд 19

Теорема. Отношение ⇒ для языка Exp является функцией
Для всех выражений е

∈ Exp справедливо, что если e ⇒ v и e ⇒ v’ , то v = v’. Это P(e).
Для доказательства применим структурную индукцию. Нужно доказать: 1) P(n) для всех чисел n. 2) При условии истинности P(e) и P(e’) доказать P(e op e’) .

Слайд 20

Первый случай
Если n ⇒ v, а для вычисления v мы могли

использовать только правило CR то n = v .
Если n ⇒ v’, то из тех же соображений получим n = v ’ .
Из n = v и n = v ’ следует, что v = v ’ .

Семантика языков программирования

Содержание

Зачем нужна формальная семантика?Чтобы точно знать возможности языка программирования. Чтобы доказывать

Эквивалентные преобразования программыЗная, что if true then C1 else C2 делает тоже

Эквивалентны ли фрагменты программы? begin C1 ; if B then C2

А эти? begin if B then C2 else C3 ; C1end if

Синтаксические категории е ∈ Exp op ∈ Op n ∈ Num Определения op ::= + | - | * | div e ::= n |

Конкретнтая операционная семантика языка Exptopostfix(N,S,[N|S]) :- number(N).topostfix(E,S,R) :- E =..

Естественная семантикаЭто аксиоматическая система, определяющая смысл каждой конструкции языка в виде

Правила, определяющие естественную семантику языка арифметических выраженийПравило CR Правило OpRn ⇒ ne ⇒

Пусть нужно вычислить значение выражения3 * 4 + 8 div (4

В конце концов, получив численную константу применим правила CR:Вычисление значения арифметических

Реализация естественной семантики языка Expeval(N,N) :- number(N).eval(E,R) :- E =.. [Op,E1,E2],

ИндукцияСвойства семантики языка программирования можно доказывать по индукции.Метод математической индукции: Чтобы доказать

ПримерПусть нужно доказать, что сумма первых n натуральных чисел равна n *

Структурная индукцияМетод математической индукции применим к натуральным числам потому, что их

Закон « map после (++)»Для всех списков xs, ys и функций

Теорема. Отношение ⇒ для языка Exp является функциейДля всех выражений е

Первый случайЕсли n ⇒ v, а для вычисления v мы могли

Похожие презентации