Денотационная семантика 0 |1|1 | 0 | 1 Mb:Mb: М b ('0') = 0, М b ('1')=1 М b ( '0') = =2 * М b ( ) М b ( 1) = =2 * М b ( ) + 1

0|1|2|3|4|5|6|7|8|9 | (0|1|2|3|4|5|6|7|8|9) Синтаксические правила: M d (0) = 0, M d ('1') = 1,,..., M d ('9') = 9 М d ( '0') = =10 * М d ( ) М d ( 1) = = 10 * М d ( ) + 1 … М d ( '9') = = 10 * М d ( ) + 9

s {,, …, } VARMAP(i k, s) == v k | + | *

M e (,s) case of => M d (, s) => if VARMAP(, s) = undef then error else VARMAP(, s) => if(M e (., s) = undef OR M e (., s) = undef) then error else if(. = '+' then M e (., s) + M e (., s) else M e (., s) * M e (., s)

М а (х = Е, s) if M e (E, s) = error then error else s' = {,,..., } where for (j = 1, 2,..., n) if i j x then v j = VARMAP(i j, s); if i j = x then v j = M e (E, s)

Аксиоматическая система Хоара {P} A {Q} Законы консеквенции: {P} A {Q}, Q=>V |- {P} A {V} {P} A {Q}, W=>P |- {W} A {Q}

Алгебраические типы данных push:stack integer stack pop:stack stack top:stack integer {undefined} empty:stack boolean size:stack integer newstack: stack Операции, определяющие тип данных: 1. Генераторы (g: not_x x) 2. Конструкторы (c: x not_x x) 3. Функции push(push(push(newstack, 1), 5), 3)

1.pop(newstack)=newstack 2.pop(push(S, I))=S 3.top(newstack)=undefined 4.top(push(S,I))=I 5.empty(newstack)=true 6.empty(push(S,I))=false 7.size(newstack)=0 8.size(push(S,I))=size(S)+1 Пример: empty(pop(push(push(newstack, 42), 17))) А2: empty(push(newstack, 42)) A6: false

Индукция типов данных 1.x, g i, c i, f i, P(y) y x. 2.P(g i )=true 3.P(y)=true => P(c i (y))=true. 4.P(y)=true, y x. Пример: P(newstack), P(push(x, i)) size(push(S,x))>size(S) – исх. утверждение Доказательство: size(S)+1>size(S)(A8) newstack:0+1>0 size(newstack)+1>size(newstack) (A7) push(S, x):size(S)+1>size(S) - гипотеза size(push(S,x))+1>size(push(S,x)) (A8) size(S)+1+1>size(S)+1

Методы спецификации программ Виды спецификаций: 1.Языки спецификации задач Языки описания требований; Языки функциональных спецификаций. 2.Языки спецификации свойств. Языки описания требований: RSL, SDL,PSL. value fact : Nat -~-> Nat fact(n) is if n = 1 then 1 else n * fact(n-1) end pre n > 0

Языки функциональных спецификаций SETL, SPECIAL, CLEAR, RDM, CIP-L, META-IV, Jota. Качества функциональных спецификаций: однозначность (точность); понятность (ясность); полнота описания задачи. Свойства языков функциональных спецификаций: выразительность; выполнимость спецификаций; доказуемость.

Методы верификации программ Свойства корректности программ: 1.Частичная корректность 2.Завершение Суть метода индуктивных утверждений: формулируются входное и выходное утверждения; строится промежуточное утверждение; формулируется теорема (условия верификации): из выведенного утверждения следует выходное утверждение; доказывается теорема.

Алгоритм доказательства правильности программ: 1.Построить структуру программы. 2.Выписать входное и выходное утверждения. 3.Сформулировать для всех циклов индуктивные утверждения. 4.Составить список выделенных путей. 5.Построить условия верификации. 6.Доказать условия верификации. 7.Доказать, что выполнение программы закончится.