Инструменты пользователя

Инструменты сайта


examination:c:question23

Вопрос №23. Верификация программы. Корректность программы.

Пусть программа задана своей моделью в виде блок-схемы Р, а ее спецификация предикатами γ,ψ. Будем считать, что программа Р частично корректна относительно γ и ψ, если для любого вектора значение входной переменной σ таково, что γ(σ) M[P](σ)≠ω выполняет ограничение ψ(σ, M[P](σ)).

Будем считать, что программа Р полностью корректна относительно γ и ψ, если для любого вектора значение входной переменной σ таково, что γ(σ) выполняет ограничение M[P](σ)≠ω, ψ(σ, M[P](σ)).

Частичная корректность Р относительно γ и ψ обозначается {γ}P{ψ}. Полная корректность Р относительно γ и ψ обозначается <γ>P<ψ>.

Лемма 2. Пусть даны программы Р и Ф=(γ,ψ). В этом случае <γ>P<ψ> тогда и только тогда, когда {γ}P{ψ} и <γ>P<Т>, т.е. для доказательства полной коррекции программы достаточно доказать ее частичную корректность и завершаемость. Заметим, что частичная и полная корректности сохраняются при замене входных предикат на более сильные и выходных предикат на более слабые.

Лемма 3. Пусть дана программа Р и предикаты γ,γ',ψ,ψ' такие, γ'→γ, ψ→ψ'/ {γ}P{ψ}⇒{γ'}P{ψ} и {γ}P{ψ'} <γ>P<ψ>⇒<γ'>P<ψ> и <γ>P<ψ'>

Лемма 4. Пусть дана программа Р. Для любых Р и γ,ψ12 выполняется следующее: из {γ}P{ψ1} и {γ}P{ψ2} следует {γ}P{ψ1∩ψ2}

examination/c/question23.txt · Последние изменения: 2014/01/15 12:09 (внешнее изменение)