close

Вход

Забыли?

вход по аккаунту

(что) Операционная семантика

код для вставкиСкачать
Сучасні проблеми інформатики
Лекція 5
Парадигми програмування
Парадигмы программирования
• Основные
–
–
–
–
Императивное
Функциональное
Алгебраическое
Логическое
• Высшие
– Параллельное
– Объектно-ориентированное
– Агентное
• Инсерционное программирование объединяет все
– Кибернетика, 1(1994), 1(2003)
2
Императивное программирование
• Структурные программы
• Программы с goto
• Программы с рекурсивными вызовами
– Функциональное программирование
• Программы с вводом-выводом
– Взаимодействие со средой
– Параллельное программирование
• Интеграция основных парадигм в императивное
3
Структурные программы
Базовые операторы
x : y
x 1 : y 1 ,..., x n : y n
–Именующие выражения
–Алгебраические выражения (арифметические, булевские, …)
–Вызовы программ (функций)
–Типы данных, многосортные алгебраические системы
Основные композиции
( P ; Q ), if ( u , P , Q ), while ( u , P )
Денотационная семантика (что)
Операционная семантика (как)
4
Денотационная семантика
R – множество имен
D – область значений
S  D
R
 R D
состояния памяти
[[ P ]]  S  S  ( R  D )  ( R  D )
смысл программы
[[ y ]] D : S  D
[[ x ]] R : S  R
[[ u ]] C : S  { 0 ,1}
[[ y ]] D ( s )  y D ( s )
значение алгебраического выражения
[[ x ]] R ( s )  x R ( s )
значение именующего выражения
[[ u ]] C ( s )  u C ( s )
значение условия
5
Рекурсивное определение [[P]]
[[ P ]]( s )  P ( s )  Ps
(( x : y ) s )( r )  if ( r  x R ( s )) then ( y D ( s )) else ( s ( r ))
( P ; Q ) s  Q ( Ps )
if ( u , P , Q ) s  if ( u C ( s )) then ( Ps ) else ( Qs )
while ( u , P )  if ( u , ( P ; while ( u , P )),  )
s  s
6
Операционная семантика
S  (   {  })  B
( x : y , s )  (  , [[ x : y ]]( s ))
( P , s )  (  , s )
Вычислительная система S
для операционной семантики
императивных программ
(( P ; Q ), s )  ( Q , s )
( P , s )  ( P , s  ), P   
(( P ; Q ), s )  (( P ; Q ), s  )
u C ( s )  1
( if ( u , P , Q ), s )  ( P , s ), ( while ( u , P ), s )  (( P ; while ( u , P )), s )
uC (s)  0
( if ( u , P , Q ), s )  ( Q , s ), ( while ( u , P ), s )  (  , s )
7
Теоремы
1. Система S детерминирована
2.
[[ P ]]( s )  s '  ( P , s ) 
 (  , s ' )
*


Индукция по длине программы и числу повторений
while – циклов
Индукция по длине истории
 (  , s ' )  (( P ; Q ), s ) 
 ( Q , s ' )
Лемма 1. ( P , s ) 
*
*
m
Лемма 2. while ( u , Q )( s ) определено   m ( while ( u , Q )( s )  Q ( s ))
3. P(s) определено 
(P, s) 
 (  , P ( s ))
*
8
1/--страниц
Пожаловаться на содержимое документа