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

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

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

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

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

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

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

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

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

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

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

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

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

ВМиК МГУ, сентябрь-декабрь 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

ВМиК МГУ, сентябрь-декабрь 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 - для перечислимых.

ВМиК МГУ, сентябрь-декабрь 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

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

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

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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко21 Product patterns: пример value ex_or : Bool > Bool ex_or(b1,b2) is case (b1,b2) of (true,false) -> true, (false,true) -> true, _ -> false end

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

ВМиК МГУ, сентябрь-декабрь 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

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

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

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

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

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

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

ВМиК МГУ, сентябрь-декабрь 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

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

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

ВМиК МГУ, сентябрь-декабрь 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

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

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

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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 10. А.К.Петренко37 Case-выражения как источник недетерминизма: пример 1 type Set == empty | add(Elem,Set) axiom forall e,e 1,e 2 : Elem, s : Set :- [no_duplicates] add(e,add(e,s)) is add(e,s) [unordered] add(e 1,add(e 2,s)) is add(e 2,add(e 1,s)) Интерес представляет вторая аксиома (продолжение на следущем слайде)

ВМиК МГУ, сентябрь-декабрь 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] результат сравнения со вторым шаблоном неоднозначен.

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

ВМиК МГУ, сентябрь-декабрь 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