Lecture-Analytical Verification (811286), страница 4
Текст из файла (страница 4)
Наиболее известным примером фундированного множества является множество натуральных чисел с отношением порядка <.Пусть P – блок-схема, а – ее входной предикат. Рассмотрим следующий метод доказательства завершимости программы P на .Шаг 1.
Точки сечения. Выберем множество точек сечения блок-схемы таким образом, чтобы каждый цикл в блок-схеме содержал, по крайней мере, одну точку сечения. Для каждой точки сечения i выберем индуктивное утверждение qi(x, y).Построим условия верификации для индуктивных утверждений qi(x, y), согласно методу, рассмотренному ранее, и докажем их корректность.Шаг 2. Оценочные функции. Выберем некоторое фундированное множество (W, ).Определим для каждой точки сечения i оценочную функцию ui(x, y) : Dx Dy W.
Для всех векторов значений переменных x и y, удовлетворяющих в точке сечения iиндуктивному утверждению qi(x, y), оценочная функция должна ставить в соответствие элемент множества W.Шаг 3. Условия завершимости. Сконструируем для каждого промежуточного базового пути , начинающегося в точке сечения i и завершающегося в точке сечения j,условия завершимости: x Dx y Dx [ qi(x, y) R(x, y) ( ui(x,y) uj(x, r(x, y) ) ) ]Условия завершимости утверждают, что если предикат qi(x, y) истинен для некоторых значений переменных x и y, и эти значения такие, что начиная из точки сечения iвычисление пойдет по пути , то результат оценочной функции uj(x, y) на значениях переменных x и y, после прохождения по пути , будет меньше результата оценочной функции ui(x, y) на исходных значениях.Теорема 2.
(Метод фундированных множеств Флойда)Пусть даны блок-схема P и ее входной предикат . Выполним следующие действия:1. Выберем точки сечения с подходящим набором индуктивных утверждений;;2. Выберем фундированное множество и найдем подходящий набор оценочных функций;;3. Построим условия верификации для всех базовых путей и условия завершимости для всех промежуточных базовых путей.Если все условия верификации и условия завершимости истинны, то блок-схема Pзавершается на .Дополнительные материалы по методам Флойда можно найти в [1,2,6].Литература1. R.
W. Floyd, "Assigning meanings to programs", Proc. Symp. Appl. Math., 19; in:J.T.Schwartz (ed.), Mathematical Aspects of Computer Science, pp. 19-32, AmericanMathematical Society, Providence, R.I., 1967.2. N. Francez, "Verification of programs", Addison-Wesley Publishers Ltd., 1992.3. Z. Manna, "Mathematical theory of computation", McGraw-Hill, 1974.4. Z. Manna, A. Pnueli, "The Temporal Logic of Reactive and Concurrent Systems",Springer-Verlag, 1991.5. Р.
Андерсон, "Доказательство правильности программ", Москва, Мир, 1982.6. Д. Жуков, "Методы верификации программ", Переславль-Залесский, 2002..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
