'

Лекция

Понравилась презентация – покажи это...





Слайд 0

Лекция Неполная спецификация и недетерминизм. Let- и Case-выражения


Слайд 1

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 2 План лекции Неполная спецификация (недоспецификация) Недетерминизм Case-выражения Шаблоны (patterns) Let-выражения Case- и Let-выражения как источник недетерминизма


Слайд 2

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 3 Самостоятельное задание


Слайд 3

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 4 Неполная спецификация Константы value x : Int, y : Int :- y ~= 0 axiom y ~= 3 Функции value f : Int -> Int axiom forall x : Int :- f(x) > x


Слайд 4

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 5 Источники неполной спецификации Возможность писать неполные спецификации является важным моментом с точки зрения процесса разработки ПО с использованием формальных методов – специфицируются лишь те аспекты, которые важны на данном уровне абстракции, а остальные можно оставить недоспецифицированными.


Слайд 5

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 6 Недетерминированные выражения С использованием оператора выбора (внешнего или внутреннего) 0 ? 1 ? 2 0 |^| 1 |^| 2 (ASCII-нотация) С использованием Let и Case let x : Nat :- x < 3 in x end (подробности позже в этой же лекции)


Слайд 6

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 7 Недетерминированная спецификация функции value f : Int -~-> Int f(x) is 0 |^| 1 |^| 2 Необходимо отметить, что такая функция не является функцией в математическом смысле, поэтому она должна быть помечена как нетотальная. Для тотальных функций в RSL условие детерминированности является обязательным.


Слайд 7

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 8 Ошибки, похожие на недетерминизм Недетерминированная спецификация тотальной функции value f : Int -> Int f(x) is 0 |^| 1 |^| 2 Недетерминированная спецификация константы является ошибкой, потому что константа – тотальная функция value x : Int = 0 |^| 1 |^| 2


Слайд 8

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 9 Case-выражения: пример value reverse : Int-list -> Int-list reverse(l) is case l of <..> -> <..> <.i.> ^ l1 -> reverse(l1) ^ <.i.> end


Слайд 9

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 10 Case-выражения: синтаксис case value_expr of pattern1 -> value_expr1, … patternn -> value_exprn end


Слайд 10

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 11 Case-выражения: семантика Ключевую роль в case-выражении играют шаблоны. Результат выражения, по которому производится выбор, проверяется на соответствие шаблонам в указанном порядке. При совпадении выполняется соответствующее выражение, результат которого и является результатом case-выражения.


Слайд 11

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 12 Шаблоны (patterns) Шаблоны выполняют две функции: Вводят новые (локальные) имена с областью видимости до конца объемлющего блока или выражения Определяют значения для введенных имен в случае совпадения проверяемого выражения с шаблоном


Слайд 12

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 13 Классификация шаблонов Literal pattern Wildcard pattern Name pattern Record pattern List pattern Product pattern


Слайд 13

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 14 Внутренние шаблоны Шаблоны строятся рекурсивно, при этом не все перечисленные типы могут использоваться во внутренних шаблонах. Во внутренних шаблонах: Нельзя использовать Name patterns Вместо них используются Equality patterns для проверки соответствия Идентификаторы, вводящие новые имена


Слайд 14

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 15 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


Слайд 15

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 16 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 - для перечислимых.


Слайд 16

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 17 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


Слайд 17

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 18 Record patterns: семантика Выражение ex соответствует шаблону id(inner_pattern1,…,inner_patternn) тогда и только тогда, когда ? ex1,…,exn :- id(ex1,…,exn) = ex где exi соответствует шаблону inner_patterni


Слайд 18

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 19 List patterns: пример (см. также вводный пример, слайд 9) value sum : Int* -> Int sum(l) is case l of <..> -> 0, <.i.> ^ l1 -> i + sum(l1) end


Слайд 19

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 20 List patterns: семантика Выражение ex соответствует шаблону <.inner_pat1,…,inner_patn.> ^ inner_pat тогда и только тогда, когда ? ex1,…,exn,l :- <.ex1,…,exn.> ^ l = ex где exi соответствует шаблону inner_pati и l соответствует шаблону inner_pat


Слайд 20

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 21 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


Слайд 21

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 22 Product patterns: семантика Выражение ex соответствует шаблону (inner_pattern1,…,inner_patternn) (n?2) тогда и только тогда, когда ? ex1,…,exn :- (ex1,…,exn) = ex где exi соответствует шаблону inner_patterni


Слайд 22

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 23 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


Слайд 23

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 24 Let-выражения Let-выражения используются для введения локальных имен Два типа Let-выражений: эксплицитные Let-выражения имплицитные Let-выражения


Слайд 24

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 25 Эксплицитные Let-выражения: синтаксис let let_binding = value_expr1 in value_expr2 end где let_binding может быть: Binding List pattern Record pattern


Слайд 25

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 26 Эксплицитные Let-выражения: пример с Binding value square_head : Int* -~-> Int* square_head(l) is let h = hd l in <.h*h.> ^ tl l end pre l ~= <..>


Слайд 26

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 27 Эксплицитные 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 ~= <..>


Слайд 27

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 28 Эксплицитные Let-выражения: пример с List pattern value square_head : Int* -~-> Int* square_head(l) is let <.h.> ^ t = l in <.h*h.> ^ t end pre l ~= <..>


Слайд 28

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 29 Эксплицитные Let-выражения: семантика с List pattern let list_pattern = value_expr1 in value_expr2 end эквивалентно case value_expr1 of list_pattern -> value_expr2 end


Слайд 29

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 30 Эксплицитные 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


Слайд 30

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 31 Эксплицитные Let-выражения: семантика с Record pattern let record_pattern = value_expr1 in value_expr2 end эквивалентно case value_expr1 of record_pattern -> value_expr2 end


Слайд 31

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 32 Имплицитные Let-выражения: синтаксис let binding : type_expr :- value_expr1 in value_expr2 end или в частном случае (без value_expr1) let typing in value_expr end


Слайд 32

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 33 Имплицитные 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


Слайд 33

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 34 Вложенные Let-выражения: синтаксис и семантика let def1,…,defn in value_expr end эквивалентно (n>1) let def1 in … let defn in value_expr end … end


Слайд 34

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 35 Вложенные Let-выражения: пример value square_head : Int* -~-> Int* square_head(l) is let h = hd l, t = tl l in <.h*h.> ^ t end pre l ~= <..>


Слайд 35

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 36 Case-выражения как источник недетерминизма Проверяемое выражение не соответствует ни одному из шаблонов (результат – swap) Используется Record pattern для типа без деструкторов и с возможностью сконструировать одинаковые значения разными способами (результат недетерминирован)


Слайд 36

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 37 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)) Интерес представляет вторая аксиома (продолжение на следущем слайде)


Слайд 37

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 38 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] результат сравнения со вторым шаблоном неоднозначен.


Слайд 38

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 39 Let-выражения как источник недетерминизма Имплицитные Let-выражения: для перечислимых типов – результат недетерминирован для неограниченных типов – результат chaos С противоречивыми условиями – результ swap Эксплицитные Let-выражения с Record pattern, эквивалентные недетерминированным Case-выражениям


Слайд 39

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко 40 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


×

HTML:





Ссылка: