- Главная
- Разное
- Дизайн
- Бизнес и предпринимательство
- Аналитика
- Образование
- Развлечения
- Красота и здоровье
- Финансы
- Государство
- Путешествия
- Спорт
- Недвижимость
- Армия
- Графика
- Культурология
- Еда и кулинария
- Лингвистика
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Детские презентации
- Информатика
- История
- Литература
- Маркетинг
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Лекция презентация
Содержание
- 1. Лекция
- 2. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 3. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко Самостоятельное задание
- 4. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 5. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 6. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 7. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 8. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 9. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 10. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 11. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 12. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 13. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 14. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 15. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 16. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 17. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 18. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 19. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 20. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 21. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 22. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 23. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 24. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 25. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 26. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 27. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 28. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 29. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 30. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 31. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 32. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 33. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 34. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 35. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 36. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 37. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 38. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 39. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
- 40. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I,
ВМиК МГУ,
сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко План лекции Неполная спецификация (недоспецификация) Недетерминизм Case-выражения Шаблоны (patterns) Let-выражения Case- и Let-выражения как источник недетерминизма
Слайд 2ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
План лекции
Неполная спецификация (недоспецификация)
Недетерминизм
Case-выражения
Шаблоны
(patterns)
Let-выражения
Case- и Let-выражения как источник недетерминизма
Let-выражения
Case- и Let-выражения как источник недетерминизма
Слайд 3ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Самостоятельное задание
Слайд 4ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Неполная спецификация
Константы
value x :
Int, y : Int :- y ~= 0
axiom y ~= 3
Функции
value f : Int -> Int axiom forall x : Int :- f(x) > x
Функции
value f : Int -> Int axiom forall x : Int :- f(x) > x
Слайд 5ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Источники неполной спецификации
Возможность писать
неполные спецификации является важным моментом с точки зрения процесса разработки ПО с использованием формальных методов – специфицируются лишь те аспекты, которые важны на данном уровне абстракции, а остальные можно оставить недоспецифицированными.
Слайд 6ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Недетерминированные выражения
С использованием оператора
выбора (внешнего или внутреннего)
0 ∏ 1 ∏ 2 0 |^| 1 |^| 2 (ASCII-нотация)
С использованием Let и Case
let x : Nat :- x < 3 in x end
(подробности позже в этой же лекции)
0 ∏ 1 ∏ 2 0 |^| 1 |^| 2 (ASCII-нотация)
С использованием Let и Case
let x : Nat :- x < 3 in x end
(подробности позже в этой же лекции)
Слайд 7ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Недетерминированная спецификация функции
value f
: Int -~-> Int
f(x) is 0 |^| 1 |^| 2
Необходимо отметить, что такая функция не является функцией в математическом смысле, поэтому она должна быть помечена как нетотальная. Для тотальных функций в RSL условие детерминированности является обязательным.
f(x) is 0 |^| 1 |^| 2
Необходимо отметить, что такая функция не является функцией в математическом смысле, поэтому она должна быть помечена как нетотальная. Для тотальных функций в RSL условие детерминированности является обязательным.
Слайд 8ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Ошибки, похожие на недетерминизм
Недетерминированная
спецификация тотальной функции
value f : Int -> Int f(x) is 0 |^| 1 |^| 2
Недетерминированная спецификация константы является ошибкой, потому что константа – тотальная функция
value x : Int = 0 |^| 1 |^| 2
value f : Int -> Int f(x) is 0 |^| 1 |^| 2
Недетерминированная спецификация константы является ошибкой, потому что константа – тотальная функция
value x : Int = 0 |^| 1 |^| 2
Слайд 9ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения: пример
value
reverse : Int-list
-> Int-list
reverse(l) is
case l of
•..> -> <..>
<.i.> ^ l1 -> reverse(l1) ^ <.i.>
end
Слайд 10ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения: синтаксис
case value_expr of
pattern1 -> value_expr1,
…
patternn -> value_exprn
end
Слайд 11ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения: семантика
Ключевую роль в
case-выражении играют шаблоны. Результат выражения, по которому производится выбор, проверяется на соответствие шаблонам в указанном порядке. При совпадении выполняется соответствующее выражение, результат которого и является результатом case-выражения.
Слайд 12ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Шаблоны (patterns)
Шаблоны выполняют две
функции:
Вводят новые (локальные) имена с областью видимости до конца объемлющего блока или выражения
Определяют значения для введенных имен в случае совпадения проверяемого выражения с шаблоном
Вводят новые (локальные) имена с областью видимости до конца объемлющего блока или выражения
Определяют значения для введенных имен в случае совпадения проверяемого выражения с шаблоном
Слайд 13ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Классификация шаблонов
Literal pattern
Wildcard pattern
Name
pattern
Record pattern
List pattern
Product pattern
Record pattern
List pattern
Product pattern
Слайд 14ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Внутренние шаблоны
Шаблоны строятся рекурсивно,
при этом не все перечисленные типы могут использоваться во внутренних шаблонах.
Во внутренних шаблонах:
Нельзя использовать Name patterns
Вместо них используются
Equality patterns для проверки соответствия
Идентификаторы, вводящие новые имена
Во внутренних шаблонах:
Нельзя использовать Name patterns
Вместо них используются
Equality patterns для проверки соответствия
Идентификаторы, вводящие новые имена
Слайд 15ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Literal + Wildcard patterns
type
Nat1 = {| n : Nat :- n > 0 |}
value fib : Nat1 -> Nat1 fib(n) is case n of 1 -> 1, 2 -> 1, _ -> fib(n-2) + fib(n-1) end
value fib : Nat1 -> Nat1 fib(n) is case n of 1 -> 1, 2 -> 1, _ -> fib(n-2) + fib(n-1) end
Слайд 16ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Name patterns
type Color ==
white | black
value invert : Color -> Color invert(c) is case c of white -> black, black -> white end
Literal pattern и Name pattern похожи. Отличие в том, что Literal используется для встроенных типов, а Name - для перечислимых.
value invert : Color -> Color invert(c) is case c of white -> black, black -> white end
Literal pattern и Name pattern похожи. Отличие в том, что Literal используется для встроенных типов, а Name - для перечислимых.
Слайд 17ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Record patterns: пример
type List
==
empty
| add( head : Color, tail : List )
value invert : List -> List invert(l) is case l of empty -> empty, add(c,l) -> add(invert(c),inverl(l)) end
value invert : List -> List invert(l) is case l of empty -> empty, add(c,l) -> add(invert(c),inverl(l)) end
Слайд 18ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Record patterns: семантика
Выражение ex
соответствует шаблону
id(inner_pattern1,…,inner_patternn)
тогда и только тогда, когда
∃ ex1,…,exn :- id(ex1,…,exn) = ex
где exi соответствует шаблону inner_patterni
id(inner_pattern1,…,inner_patternn)
тогда и только тогда, когда
∃ ex1,…,exn :- id(ex1,…,exn) = ex
где exi соответствует шаблону inner_patterni
Слайд 19ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
List patterns: пример
(см. также
вводный пример, слайд 9)
value sum : Int* -> Int sum(l) is case l of <..> -> 0, <.i.> ^ l1 -> i + sum(l1) end
value sum : Int* -> Int sum(l) is case l of <..> -> 0, <.i.> ^ l1 -> i + sum(l1) end
Слайд 20ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
List patterns: семантика
Выражение ex
соответствует шаблону
<.inner_pat1,…,inner_patn.> ^ inner_pat
тогда и только тогда, когда
∃ ex1,…,exn,l :- <.ex1,…,exn.> ^ l = ex
где exi соответствует шаблону inner_pati и l соответствует шаблону inner_pat
<.inner_pat1,…,inner_patn.> ^ inner_pat
тогда и только тогда, когда
∃ ex1,…,exn,l :- <.ex1,…,exn.> ^ l = ex
где exi соответствует шаблону inner_pati и l соответствует шаблону inner_pat
Слайд 21ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Product patterns: пример
value
ex_or :
Bool >< Bool -> Bool
ex_or(b1,b2) is
case (b1,b2) of
(true,false) -> true,
(false,true) -> true,
_ -> false
end
Слайд 22ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Product patterns: семантика
Выражение ex
соответствует шаблону
(inner_pattern1,…,inner_patternn) (n≥2)
тогда и только тогда, когда
∃ ex1,…,exn :- (ex1,…,exn) = ex
где exi соответствует шаблону inner_patterni
(inner_pattern1,…,inner_patternn) (n≥2)
тогда и только тогда, когда
∃ ex1,…,exn :- (ex1,…,exn) = ex
где exi соответствует шаблону inner_patterni
Слайд 23ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Equality patterns
(см. слайды 16
и 17)
value invert : List -> List invert(l) is case l of empty -> empty, add(=white,l1) -> add(black,invert(l1)), add(=black,l1) -> add(white,invert(l1)) end
value invert : List -> List invert(l) is case l of empty -> empty, add(=white,l1) -> add(black,invert(l1)), add(=black,l1) -> add(white,invert(l1)) end
Слайд 24ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Let-выражения
Let-выражения используются для введения
локальных имен
Два типа Let-выражений:
эксплицитные Let-выражения
имплицитные Let-выражения
Два типа Let-выражений:
эксплицитные Let-выражения
имплицитные Let-выражения
Слайд 25ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: синтаксис
let let_binding
= value_expr1 in
value_expr2
end
где let_binding может быть:
Binding
List pattern
Record pattern
где let_binding может быть:
Binding
List pattern
Record pattern
Слайд 26ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: пример с
Binding
value
square_head : Int* -~-> Int*
square_head(l) is
let h = hd l in
<.h*h.> ^ tl l
end
pre l ~= <..>
Слайд 27ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: пример с
Binding - 2
value
square_head : Int* -~-> Int*
square_head(l) is
let (h,t) = (hd l,tl l) in
<.h*h.> ^ t
end
pre l ~= <..>
Слайд 28ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: пример с
List pattern
value
square_head : Int* -~-> Int*
square_head(l) is
let <.h.> ^ t = l in
<.h*h.> ^ t
end
pre l ~= <..>
Слайд 29ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: семантика с
List pattern
let list_pattern = value_expr1 in
value_expr2
end
эквивалентно
case value_expr1 of
list_pattern -> value_expr2
end
Слайд 30ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: пример с
Record pattern
type Set == empty | add (Elem,Set)
value
choose : Set -~-> Elem
choose(s) is
let add(e,_) = s in
e
end
pre s ~= empty
Слайд 31ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Эксплицитные Let-выражения: семантика с
Record pattern
let record_pattern = value_expr1 in
value_expr2
end
эквивалентно
case value_expr1 of
record_pattern -> value_expr2
end
Слайд 32ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Имплицитные Let-выражения: синтаксис
let binding
: type_expr :- value_expr1
in value_expr2
end
или в частном случае (без value_expr1)
let typing in value_expr end
или в частном случае (без value_expr1)
let typing in value_expr end
Слайд 33ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Имплицитные Let-выражения: примеры
value
choose :
Elem-set -~-> Elem
choose(s) is
let e : Elem :- e isin s in e end
pre s ~= {}
value choose_char : Unit -~-> Char choose_char() is let c : Char in c end
value choose_char : Unit -~-> Char choose_char() is let c : Char in c end
Слайд 34ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Вложенные Let-выражения: синтаксис и
семантика
let def1,…,defn in value_expr end
эквивалентно (n>1)
let def1 in
…
let defn in
value_expr
end
…
end
Слайд 35ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Вложенные Let-выражения: пример
value
square_head :
Int* -~-> Int*
square_head(l) is
let h = hd l, t = tl l in
<.h*h.> ^ t
end
pre l ~= <..>
Слайд 36ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения как источник недетерминизма
Проверяемое
выражение не соответствует ни одному из шаблонов (результат – swap)
Используется Record pattern для типа без деструкторов и с возможностью сконструировать одинаковые значения разными способами (результат недетерминирован)
Используется Record pattern для типа без деструкторов и с возможностью сконструировать одинаковые значения разными способами (результат недетерминирован)
Слайд 37ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения как источник недетерминизма:
пример 1
type Set == empty | add(Elem,Set)
axiom forall e,e1,e2 : Elem, s : Set :-
[no_duplicates]
add(e,add(e,s)) is add(e,s)
[unordered]
add(e1,add(e2,s)) is add(e2,add(e1,s))
Интерес представляет вторая аксиома (продолжение на следущем слайде)
Слайд 38ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Case-выражения как источник недетерминизма:
пример – 2
type Res == is_empty | element(e : Elem)
value
choose : Set -~-> Res
choose(s) is
case s of
empty -> is_empty,
add(e,s1) -> element(e)
end
В сочетании с аксиомой [unordered] результат сравнения со вторым шаблоном неоднозначен.
Слайд 39ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Let-выражения как источник недетерминизма
Имплицитные
Let-выражения:
для перечислимых типов – результат недетерминирован
для неограниченных типов – результат chaos
С противоречивыми условиями – результ swap
Эксплицитные Let-выражения с Record pattern, эквивалентные недетерминированным Case-выражениям
для перечислимых типов – результат недетерминирован
для неограниченных типов – результат chaos
С противоречивыми условиями – результ swap
Эксплицитные Let-выражения с Record pattern, эквивалентные недетерминированным Case-выражениям
Слайд 40ВМиК МГУ,
сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 10. А.К.Петренко
Let-выражения как источник недетерминизма:
примеры
Для перечислимых типов:
let c : Color in c end
is black |^| white
Для неограниченных типов:
let x : Int in x end
is chaos
С противоречивыми условиями:
let x : Nat :- x < -5 in x end
is swap
