Евгений Корныхин - Формальная спецификация программ (Евгений Корныхин - Формальная спецификация программ.pdf), страница 11
Описание файла
PDF-файл из архива "Евгений Корныхин - Формальная спецификация программ.pdf", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 11 страницы из PDF
Аналитическая верификацияSqrt()1 (1 , 2 , 3 ) ← (0, 0, 1)2 while3do 2 ← 2 + 34if 2 > 5then break6else (1 , 3 ) ← (1 + 1, 3 + 2)7 ← 14.1.12 (1 , 2 ) (1 > 0) ∧ (2 > 0), (1 , 2 , 1 , 2 ) (0 ≤2 < 2 ) ∧ (1 = 1 · 2 + 2 )Division(1 , 2 )1 (1 , 2 , 3 ) ← (0, 0, 1 )2 while 3 ̸= 03do 1 ← (2 + 1 = 2 ) ℎ (1 + 1) 142 ← (2 + 1 = 2 ) ℎ 0 (2 + 1)5 3 ← 3 − 16 (1 , 2 ) ← (1 , 2 )4.1.13() , (, ) ( = 2 )Square()1 (1 , 2 , 3 ) ← (0, 1, 1 − )2 while 3 < 3do if (2 )4then 1 ← 1 + 25(2 , 3 ) ← (2 + 1, 3 + 1)6 ← 1() истинно тогда и только тогда, когда нечетно.4.1.14() , (, ) ( 3 ≤ < ( + 1)3 )4.1.
Методы ФлойдаCubert()1 (1 , 2 , 3 ) ← (0, 0, 1)2 while3do 2 ← 2 + 34if 2 > 5then break6else 1 ← 1 + 173 ← 3 + 618 ← 14.1.15() ( < 102), (, ) ( = 91)Century()1 (1 , 2 ) ← (, 1)2 while 1 < 101 ∨ 2 ≠ 13do if 1 > 1004then (1 , 2 ) ← (1 − 10, 2 − 1)5else (1 , 2 ) ← (1 + 11, 2 + 1)6 ← 1 − 104.1.16() ( > 1), (, ) ( = 3 )Qube()1 (1 , 2 , 3 ) ← (, 1, )2 while3do if 2 < 34then (1 , 2 ) ← (1 + , 2 + 1)5else if 3 = 6then 3 ← 17else break8 ← 14.1.17() , (, ) ( = 2 )8788Глава 4.
Аналитическая верификацияSquare()1 (1 , 2 ) ← (, 1)2 while 2 < 3do if 22 ≤ 4then (1 , 2 ) ← (21 , 22 )5else (1 , 2 ) ← (1 + , 2 + 1)6 ← 14.1.18(1 , 2 ) , (1 , 2 , ) ( = 1 2 ) (00 1)Power()1 (1 , 2 , 3 ) ← (1 , 2 , 1)2 while 2 ̸= 03do if (2 )4then (2 , 3 ) ← (2 − 1, 1 · 3 )5else (1 , 2 ) ← (1 · 1 , 2 /2)6 ← 3() истинно тогда и только тогда, когда нечетно.Приложение АПриоритет операций вRSLОперации с меньшим приоритетом обрабатываются раньше.Приоритет операций в типовых выраженияхприоритет4321операторы,−→ ]−→×-set -infsetассоциативностьправаяправая⋆ Приоритет операций в выражениях со значениемприоритетоператорыассоциативность13правая∀ ∃ ∃!12≡11[] ⌈⌉ || ∦правая10;правая9:=8⇒правая7∨правая6∧правая5≠=><>6⊂⊃⊆⊇∈∈/∧4+ − ∖ ∪†левая3*/ ∘ ∩левая2↑1∼ префиксы суффиксы89Литература[1] Ахо, .
. Структуры данных и алгоритмы / . . Ахо, . . Хопкрофт,. . Ульман. — Вильямс, 2003.[2] Кормен, . Алгоритмы: построение и анализ / . Кормен, . Лейзерсон,. Ривест. — МЦНМО, 2002.[3] Непейвода, . . Практическая логика / . . Непейвода. — Новосибирск,НГУ, 2000.[4] Шень, .
Программирование: теоремы и задачи / . Шень. — 2 edition. —МЦНМО, 2004.90.
