Говорят, что
является частично правильной относительно ее спецификации, заданной
в виде утверждений
и
(или, что то же самое, обладает свойством частичной правильности {
}P{
}),
если для любых начальных значений переменных, относительно которых справедливо
,
выполнение действия
(если оно определено) дает такие конечные значения переменных, для которых
истинно утверждение
.
Примеры свойств:
,
,
для любых
и
.
Заметим, что частичная правильность ничего не говорит о завершаемости .
Так, например, в последнем свойстве оператор не применим, если сумма
превышает MaxInt.
Свойство правильности программы
относительно внешней ее спецификации, заданной в виде утверждений
и
,
означает справедливость свойства частичной правильности {
},
а также свойства завершаемости программы
-- нормального завершения выполнения программы
на любом начальном состоянии, удовлетворяющем утверждению
.
Идея метода промежуточных утверждений для доказательства частичной правильности Паскаль-программ состоит в построении исчисления свойств частичной правильности программ и их частей, аксиомами в котором выступают свойства элементарных операторов (операторов присваивания и пустых операторов), а правила вывода связаны с другими конструкциями языка и позволяют выводить свойства этих конструкций из свойств составляющих его компонент или операторов присваивания (как это имеет место для операторов ввода-вывода).
При этом ход построения доказательства заданного свойства частичной правильности всей Zonnon-программы (или ее части) может состоять в последовательном применении правил вывода свойств, сводящих исходное свойство к некоторым свойствам образующих ее частей -- в конечном счете к группе свойств частичной правильности составляющих ее операторов присваивания, либо в его выводе из свойств операторов присваивания. Цель -- построить вывод заданного свойства частичной правильности. В этом доказательстве (выводе) могут использоваться также все традиционные аксиомы и правила вывода соответствующего логического исчисления и той области (например, арифметики), к которой относится задача, решаемая программой.
Семантика пустого оператора
описывается очевидной аксиомой пустого оператора: {
}
{
}
для любого утверждения
В соответствии с семантикой оператора присваивания
имеем следующую аксиому оператора присваивания: {
},
где
и
-- любая пара утверждений таких, что
-- утверждение, получающееся из
подстановкой выражения
вместо вхождения переменной
Например, справедливы свойства:
.
Следующие два правила завершают построение исчисления свойств Zonnon-программ, использующих лишь уже рассмотренные конструкции языка; в дальнейшем они будут дополнены правилами и для других конструкций.
Правило вывода следствий формулируется следующим образом. Пусть
для фрагмента программы
имеет место
{},
и пусть утверждение
сильнее
,
а утверждение
слабее
.
Тогда имеет место {
}.
Например, из рассмотренных выше свойств оператора присваивания
можно вывести свойства:
,
.
Правило вывода свойств последовательности операторов имеет следующий
вид. Пусть
и
-- последовательности операторов, обладающие соответственно свойствами
{
}
и {
}.
Тогда для последовательности
имеет место свойство {
}.
В качестве примера применения метода промежуточных утверждений покажем,
что
для любых целых чисел A
и B
По аксиоме оператора присваивания имеем следующие свойства операторов,
составляющих анализируемую последовательность:
.
Применяя правило вывода следствий, из последнего свойства получаем
.
Отсюда и из первых двух свойств по правилу вывода свойств последовательности операторов получаем: сначала --
,
а затем --
.
Аналогичными правилами можно доказывать правильность программ. Для этого в ходе доказательства следует проверять, что представленные программой последовательности операций на соответствующих состояниях памяти могут быть выполнены. Такая проверка для всех рассмотренных языковых конструкций сводится к анализу значений выражений на состояниях памяти, заданных с помощью утверждений, и во многих конкретных случаях легко реализуется.
В дальнейшем в тексты программ мы будем включать утверждения, размещая
их в скобках комментариев. Такие формализованные комментарии называются
аннотациями;
они определяют те свойства состояний, которые справедливы в соответствующие
моменты выполнения программы. Аннотированная программа может выступать
в качестве доказательства своей правильности. Например, программу
возведения в десятую степень можно дополнить следующими аннотациями:
module X10D;
var A,B : integer;
begin (*
*)
read(A); (* {}*)
B := AA;
(* {
}*)
B := BB;
(*{
}*)
B := BA;
(* {
}*)
B := BB;
(*{
}*)
write(B) (* {}*)
end X10D.
Нетрудно убедиться, что программа удовлетворяет спецификации "Быстрое
возведение в десятую степень", просто показав для каждой тройки (аннотация1,
оператор, аннотация2) справедливость свойства {утверждение1} оператор {утверждение2}
и соответствующего свойства завершаемости. Вместе с тем следует отметить,
что программа X
перегружена утверждениями и часть ее аннотаций очевидна и легко восстановима
из текста программы. Это говорит о том, что не обязательно включать в текст
программы все известные вам утверждения о программе; нужно вставлять достаточно
утверждений, чтобы программа стала понимаемой, однако не так много, чтобы
она затерялась в них.
Следующий пример показывает, что иногда при описании свойств программ удобно использовать дополнительные ("внепрограммные") переменные. Рассмотрим следующую старинную задачу о переправе на другой берег волка, козы и капусты. На левом берегу реки находятся лодочник с лодкой, волк, коза и капуста. Их нужно переправить на правый берег. Лодка, помимо лодочника, вмещает лишь одного из троих (волка, козу или капусту). При этом нельзя оставлять наедине волка с козой, а также козу с капустой. Правильность следующего решения этой задачи очевидна из аннотаций, использующих две дополнительные переменные ЛевыйБерег и ПравыйБерег:
module ПЕРЕПРАВА;
begin
(*{ЛевыйБерег=(лодочник, волк, коза, капуста), ПравыйБерег=()}*)end ПЕРЕПРАВА.
writeln('Перевезти козу.');
(*{ЛевыйБерег=(волк, капуста), ПравыйБерег=(лодочник, коза)}*)
writeln('Переправиться без груза.');
(*{ЛевыйБерег=(лодочник, волк, капуста), ПравыйБерег=(коза)}*)
writeln('Перевезти волка.');
(*{ЛевыйБерег=(капуста), ПравыйБерег=(лодочник, волк, коза)}*)
writeln('Перевезти козу.');
(*{ЛевыйБерег=(лодочник, коза, капуста), ПравыйБерег=(волк)}*)
writeln('Перевезти капусту.');
(*{ЛевыйБерег=(коза), ПравыйБерег=(лодочник, волк, капуста)}*)
writeln('Переправиться без груза.');
(*{ЛевыйБерег=(лодочник, коза), ПравыйБерег=(волк, капуста)}*)
writeln('Перевезти козу.')
(*{ЛевыйБерег=(), ПравыйБерег=(лодочник, волк, коза, капуста)}*)
Next:2.3.5
Упражнения Up:2.3
Доказательство свойств программ
Previous:2.3.3
Утверждения как множества