Lecture-Analytical Verification (811286), страница 3
Текст из файла (страница 3)
После прохождения этого пути значение переменной y2уменьшится на положительную величину (x2). С другой стороны, значение переменной y2останется неотрицательным. И так как не существует бесконечной убывающей последовательности неотрицательных целых чисел, то цикл B-D-B не может выполняться бесконечное число раз, если значения входных переменных программы удовлетворяли предикату .
Следовательно, программа целочисленного деления завершается на входном предикате .Мы доказали, что {0}Pdiv{} и PdivT. Отсюда, по леммам 2 и 3, следует Pdiv.То есть полная корректность программы целочисленного деления относительно и .Методы доказательства корректности программМы рассмотрели доказательство полной корректности программы на примере программы целочисленного деления. Теперь мы определим методы доказательства корректности программ, представленных в виде блок-схем, в общем случае.Как и в примере, доказательство полной корректности будет проводиться в два этапа.
Сначала доказывается частичная корректность программы. Для этого мы будем использовать метод индуктивных утверждений Флойда. Вторым шагом, проводится доказательство завершаемости программы. Для решения этой задачи мы будем использовать метод фундированных множеств Флойда.Метод индуктивных утверждений ФлойдаПусть P блок-схема, а – путь в этой блок-схеме, начинающийся со связки e0 изавершающийся связкой ek. Дадим несколько вспомогательных определений. Определим предикат допустимости R(x,y) : Dx Dy { Т, F } и функцию пути r(x,y) : Dx Dy Dy.Предикат допустимости R(x,y) определяет, какое должно быть значение входных и промежуточных переменных в начале пути, чтобы дальнейшее вычисление шло по пути .
Функция пути r(x,y) определяет, как изменятся значения промежуточных переменных в результате исполнения всех операторов блок-схемы лежащих на пути .Наиболее простым способом вычисления предиката допустимости R(x,y) и функции пути r(x,y) является метод обратных подстановок.Пусть последовательность операторов на пути есть n1, …, nk. Для каждого m { 1, …, k+1 }, определим предикат Rm(x,y) и функцию r m(x,y). При этом для m k,функция r(x,y) будет являться функцией пути, проходящего через операторы nm, …, nk, а предикат Rm(x,y) будет являться предикатом допустимости для этого же пути.Таким образом,R(x,y) R1(x,y)r(x,y) r1(x,y)Предикаты Rm(x,y) и функции r(x,y) мы определим индукцией по m.Базис индукции:Rk+1( x, y ) Trk+1( x, y ) yИндуктивное предположение:Предположим, что Rm+1(x,y) и rm+1(x,y) уже определены для некоторого m { 2, …, k+1 }.Индуктивный переход:Определим в зависимости Rm(x,y) и rm(x,y) от оператора nm: Если nm – оператор присваивания ASSIGNMENT: y g( x, y ), то Rm( x, y ) Rm+1( x, g( x, y ) )rm( x, y ) rm+1( x, g( x, y ) ) Если nm – условный оператор TEST: t( x, y ) и связка em помечена символом T, тоRm( x, y ) Rm+1( x, y )rm( x, y ) rm+1( x, y ) t( x, y ) Если nm – условный оператор TEST: t( x, y ) и связка em помечена символом F, тоRm( x, y ) Rm+1( x, y )rm( x, y ) rm+1( x, y ) t( x, y ) Если nm – оператор соединения JOIN, тоRm( x, y ) Rm+1( x, y )rm( x, y ) rm+1( x, y )Заметим, что операторы других типов (начальный и завершающий) не могут встречаться на пути, так как они не имеют либо входящих, либо выходящих связок.Для этих операторов, мы расширим определения предиката допустимости и функции пути.
Если началом первой связки пути является начальный оператор START: y f( x ),то мы будем говорить, что предикат допустимости R'(x) R( x, f( x ) ), а функция пути r'(x) r(x, f( x ) ). Если концом последней связки пути является завершающий оператор HALT: z h( x, y ), то мы будем говорить, что функция пути r''( x, y ) h( x, r( x, y ) )( r''( x, y ) : Dx Dy Dz ).Индуктивные утверждения. Пусть P – блок-схема, а = ( , ) – ее спецификация. Рассмотрим следующий метод доказательства частичной корректности программы Pотносительно спецификации .Шаг 1.
Точки сечения. Выберем подмножество связок блок-схемы. Эти связки мы будем называть точками сечения. Выбранное множество точек сечения должно быть таким, чтобы каждый цикл в блок-схеме содержал, по крайней мере, одну точку сечения.Все ориентированные пути между точками сечения, не содержащие других точек сечения, мы будем называть промежуточными базовыми путями. Пути, начинающиеся в начальном операторе, заканчивающиеся в точке сечения и не содержащие других точек сечения, мы будем называть начальными базовыми путями. Пути, начинающиеся в точке сечения, заканчивающиеся в одном из завершающихся операторов и не содержащие других точек сечения, мы будем называть конечными базовыми путями.Шаг 2. Индуктивные утверждения.
Выберем для каждой точки сечения iпредикат pi(x, y), который характеризует отношение между переменными блок-схемы при прохождении данной связки. Часто, эти предикаты называют индуктивными утверждениями. Кроме того, свяжем входной предикат (x) с начальным оператором блок-схемы, а выходной предикат (x, z) – со всеми завершающими операторами.Шаг 3. Условия верификации. На третьем шаге, сконструируем для каждого промежуточного базового пути , начинающегося в точке сечения i и завершающегося в точке сечения j, условия верификации: x Dx y Dx [ pi(x, y) R(x, y) pj( x, r(x, y) ) ]Эти условия утверждают, что если предикат pi(x, y) истинен для некоторых значений переменных x и y, и эти значения такие, что начиная из точки сечения i вычисление пойдет по пути , то предикат pj(x, y) будет истинен для значений переменных x и y,после прохождения по пути .Для начального базового пути , завершающегося в точке сечения j, условия верификации будут выглядеть следующим образом: x Dx [ (x) R'(x) pj( x, r'(x) ) ]В этом случае, условия утверждают, что если входной предикат (x) истинен для некоторых значений входных переменных, и эти значения такие, что начальное вычисление пойдет по пути , то предикат pj(x, y) будет истинен для значений переменных x и y, после прохождения по пути .Для конечного базового пути , начинающегося в точке сечения i, условия верификации конструируются следующим образом: x Dx y Dx [ pi(x, y) R(x, y) ( x, r''(x, y) ) ]Здесь, условия верификации утверждают, что если предикат pi(x, y) истинен для некоторых значений переменных x и y, и эти значения такие, что начиная из точки сечения i вычисление пойдет по пути , то предикат (x, z) будет истинен для значений переменных x и z, после завершения работы блок-схемы при прохождения по пути .Для вырожденного случая, когда начальный базовый путь является в то же время завершающим базовым путем, условия верификации будут выглядеть следующим образом: x Dx [ (x) R'(x) ( x, r''( x, r'(x) ) ) ]В этом случае, условия утверждают, что если входной предикат (x) истинен для некоторых значений входных переменных, и эти значения такие, что вычисление пойдет по пути , то выходной предикат (x, z) будет истинен для значений переменных x и z,после завершения работы блок-схемы при прохождения по пути .Лемма 5.
Пусть все условия верификации истинны. Пусть дано вычисление блоксхемы P, входные переменные которого удовлетворяют входному предикату . Тогда для каждого прохода вычисления Ck – Ck+1 через точку сечения i, предикат pi(x, y) будет истинен на значениях переменных x и y в конфигурации Ck.Теорема 1. (Метод индуктивных утверждений Флойда)Пусть даны блок-схема P и ее спецификация = ( , ).
Выполним следующие действия:1. Выберем точки сечения;;2. Найдем подходящий набор индуктивных утверждений;;3. Построим условия верификации для всех базовых путей.Если все условия верификации истинны, то блок-схема P частично-корректна относительно спецификации .Все шаги метода Флойда, за исключением второго, могут быть выполнены относительно автоматически.
А вот выбор подходящего набора индуктивных утверждений требует хорошего понимания функционирования программы и поэтому сложно поддается автоматизации.Метод фундированных множеств ФлойдаДалее мы рассмотрим метод доказательства завершаемости программ, представленных в виде блок-схем.Напомним некоторые определения.
Частично-упорядоченным множеством ( W, )называется непустое множество W и любое бинарное отношение на этом множестве, которое удовлетворяет следующим свойствам:1. Для всех a, b, c W из a b и b c следует a c [Транзитивность]2. Для всех a, b W из a b следует ( b a ) [Асиметричность]3. Для всех a W ( a a ) [Иррефлексивность]Частично-упорядоченное множество ( W, ) называется фундированным, если не существует бесконечно убывающей последовательности его элементов a0 a1 a2 ….
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
