Учебное пособие по методам Флойда, страница 2

Из оператора присваивания выходит ровно 1 дуга,помеченная символом .c. Из условного оператора выходит ровно 2 дуги, причемодна из них помечена символом T, а другая – символомF.d. Изоператорасоединениявыходитровно1дуга,помеченная символом .e. Из завершающего оператора не выходит ни одной дуги.4.

Число связок, входящих в каждый оператор, соответствуетего типу:a. В начальный оператор не входит ни одна дуга.b. В оператор присваивания, условный и завершающийоператор входит ровно одна дуга.c. В оператор соединения входит не менее одной дуги.Заметим, что для каждого оператора n и символа s в корректноопределенной блок-схеме (V, N, E) существует не более одногооператора n', что ( n, s, n' )  E. Такой оператор n' (если онсуществует) мы будем называть последователем оператора n попометке s и обозначать как succ(n, s).10Далее мы будем рассматривать только корректно-определенныеблок-схемы, и, поэтому, слово «корректно-определенная» будетопускаться.В графическом представлении блок-схем мы будем опускатьнекоторые детали.

Например, ребра, помеченные символом , будутизображаться без соответствующей метки. Как правило, будутопускатьсяметкисоединениянеоператороввсевходящиеблок-схемы,аребраизображатьсябудутвоператорахсострелками на конце.START:( y1, y2 )  ( 0, x1 )Ty2  x2FHALT:( z1, z2 )  ( y1, y2 )( y1, y2 )  ( y1+1, y2- x2 )Рисунок 2. Блок-схема программы целочисленного деленияДля определения функций будет использоваться следующаянотация:( y1, y2, …, yb )  ( f1( x, y ), f2( x, y ), …, fb( x, y ) )Пример графического представления блок-схем можно увидетьнарисунке 2,гдепредставленаблок-схемапрограммыцелочисленного деления.

В этом примере множество переменных V= {x1, x2, y1, y2, z1, z2} состоит из двух входных, двух промежуточныхи двух выходных переменных. Доменом всех переменных являетсямножество целых чисел.11Далеебезограниченияобщностипод«программами»понимаются их блок-схемы.Семантика блок-схемКонфигурацией программы P будем называть пару ( ,  ), где  P – метка текущего оператора программы, = ( d1, d2, …, da+b )  Dx+  Dy+ – вектор значений входных ипромежуточных переменных программы.ЕслиDx+Dy+–векторзначенийвходныхипромежуточных переменных программы, а функция f : Dx+  Dy+ Dy+ вычисляет новые значения переменных y, то вектор значенийвходных и промежуточных переменных программы, полученныйпутем замены в  значений переменных y на f(), мы будемобозначать как [y  f(x, y)].Конечная или бесконечная последовательность конфигураций{ Ci | i = 1, …, n, … } программы P называется вычислением, если1.

Метка первой конфигурации программы является меткойначального оператора.2. Значения всех входных переменных программы являютсяопределенными ( ) и неизменными во всех конфигурацияхвычисления.3. Значенияпромежуточныхпеременныхвпервойконфигурации равны  (не определены).4. Если метка i текущего оператора конфигурации C i являетсяметкой начального оператора START: y  f(x), то следующая12конфигурация Ci+1 состоит из метки оператора succ(ni, ) ивектора значений переменных i+1 = i[y  f(x)].5.

Если метка i текущего оператора конфигурации C i являетсяметкой оператора присваивания ASSIGN: y  g(x, y), тоследующая конфигурация Ci+1 состоит из метки оператораsucc(ni, ) и вектора значений переменных i+1 = i[y  g(x,y)].6. Если метка i текущего оператора конфигурации C i являетсяметкой условного оператора TEST: t(x, y) и предикат t(x, y)при значениях переменных iпринимает значение T, тоследующая конфигурация Ci+1 состоит из метки оператораsucc(ni, T) и вектора значений переменных i+1 = i.7. Если метка i текущего оператора конфигурации C i являетсяметкой условного оператора TEST: t(x, y) и предикат t(x, y)при значениях переменных iпринимает значение F, тоследующая конфигурация Ci+1 состоит из метки оператораsucc(ni, F) и вектора значений переменных i+1 = i.8.

Если метка i текущего оператора конфигурации C i являетсяметкойоператорасоединенияJOIN,тоследующаяконфигурация Ci+1 состоит из метки оператора succ(ni, ) ивектора значений переменных i+1 = i.9. Если метка i текущего оператора конфигурации C i являетсяметкой завершающего оператора HALT: z  h(x, y), то Ciявляется последней конфигурацией вычисления.10.ЕсливконфигурацииCi+1значениекакой-либопромежуточной переменной равно , то это последняяконфигурация вычисления.13Тем самым, возможны три вида вычислений:1.

конечные последовательности конфигураций, в последнейконфигурации никакие значения переменных не равны ;2. конечные последовательности конфигураций, в последнейконфигурации значения некоторых переменных равны ;3. бесконечные последовательности конфигураций.Лемма 1. Для каждой блок-схемы P и вектора значений еевходных переменных x существует единственное вычисление, впервой конфигурации которого значения входных переменных равныx.Каждой блок-схеме P мы поставим в соответствие функциюM[P]извходногодоменаблок-схемыввыходнойдомен,расширенный специальным значением  (M[P]: Dx  Dz+).

Есливычисление блок-схемы P на векторе входных переменных xявляется конечным, в последней конфигурации которого нет , изавершается на операторе HALT, то функция M[P] (x) принимаетзначение h(x, yn), где h – функция завершающего операторапоследней конфигурации вычисления, а yn – вектор значенийпромежуточныхпеременныхизпоследнейконфигурациивычисления. В противном случае функция M[P] (x) принимаетзначение .Задачи и упражненияВ данных задачах предполагается, что доменом всех входных ивыходныхфункции,переменныхприписанныеявляетсямножествооператорам,14целыхдолжнычисел,азадаватьсяарифметическимиформуламинадоперациямисложения,вычитания и умножения и операциями сравнения.1.1.1 Перечислите все операторы в блок-схеме целочисленногоделения, приведенной на рисунке 2.1.1.2 Приведитеединственнойблок-схемувыходнойсединственнойпеременной,входнойвычисляющуюиквадратвходной переменной.1.1.3 Приведитеблок-схемусединственнойвходнойиединственной выходной переменной, вычисляющую факториалзначения входной переменной, если оно неотрицательно.

Можнопредполагать, что отрицательные значения входной переменной небудут использоваться в вычислениях этой блок-схемы.1.1.4 Приведитеблок-схемусединственнойединственной выходной переменной, вычисляющуювходной[ ]x+1xи, где х— это значение входной переменной, для положительных значенийх. Можно предполагать, что неположительные значения х не будутиспользоваться в вычислениях этой блок-схемы.1.1.5 Приведитеблок-схемусединственнойединственной выходной переменной, вычисляющуювходнойx⋅( x+1)2и, гдех — это значение входной переменной, для неотрицательныхзначений х. Можно предполагать, что отрицательные значения х небудут использоваться в вычислениях этой блок-схемы.151.1.6 Приведитеблок-схемусединственнойвходнойпеременной, не завершающуюся на бесконечном числе ее значений.1.1.7 Приведите блок-схему с двумя входными переменными x1и x2 и единственной выходной переменной, которая вычисляетколичество простых чисел между x1 и x2.1.1.8 Ответьтенавопрос,зацикливаетсялиблок-схема,изображенная на рисунке 2.

Если да, то приведите всевозможныепарызначенийвходныхпеременных,прикоторыхоназацикливается. Если нет, обоснуйте свой ответ.1.1.9 Приведите пример блок-схемы каждого из следующихвидов, если они существуют:a) в которых количество циклов меньше числа операторовсоединения;b) в которых количество циклов равно числу операторовсоединения;c) в которых количество циклов больше числа операторовсоединения.1.2 Математическая модель требованийМатематическую модель требований к верифицируемой программе мы будем называть спецификацией программы. Семантикаспецификации состоит в формальном описании требований к поведению программы.Требований к поведению программ может быть огромное множество, но в данном разделе мы будем рассматривать только тре-16бования к функциональности программ.

Под требованиями кфункциональности понимаются ограничения на результат вычисления программы в зависимости от значений ее входных данных.Входной и выходной предикатыСпецификацией  программы над переменными V мы будемназывать два предиката:входной предикат : Dx  { Т, F }выходной предикат : Dx  Dz  { Т, F }Выходной предикат (или постусловие) определяет, какие значения выходных переменных программы являются допустимыми(правильными) относительно значений входных переменных. Авходной предикат (или предусловие) определяет, при каких значениях входных переменных требуется выполнение ограничений,описанных в выходном предикате.Задачи и упражненияВ двух первых задачах предполагается, что доменом всехвходных и выходных переменных является множество целыхчисел, а все используемые в качестве предикатов функциидолжны быть формально определены. Можно считать априорным, что уже формально определены следующие арифметические операции над целыми числами: сложение, вычитание,умножение — а также операции сравнения (равно, неравно,больше, меньше и т.

п.).1.2.1 Опишите словами требования, описанные каждой изследующих спецификаций:a) (x) = (x > 0)(x, z) = (x · x = z)17b) (x) = (x > 0) (x, z) = (0 ≤ z < x)c) (x1, x2) = (x1 > x2 + 1)(x1, x2, z) = (x1 > z > x2 )d) (x) = (x > 0) (x, z) = (x < z < 0)1.2.2 Дайте формальную спецификацию каждого из следующихтребований:a) программа должна вычислять модуль данного ей числа.b) программадлядвухданныхцелыхчиселдолжнавычислять максимальное из них.c) программа должна для двух данных ей положительныхцелых чисел вычислять их сумму, а для двух данных ейотрицательных целых чисел — произведение.d) программа должна для любого неотрицательного целогочиславычислятьближайшееснизуприближениекквадратному корню из него.e) программа должна для любого положительного целогочисла большего единицы вычислять его максимальныйпростой делитель.f) программа должна для двух заданных положительныхцелых чисел вычислять количество простых чисел междуними.1.2.3 Обоснованно ответьте на следующий вопрос.

Является лидля любых спецификаций вида (a, b) над переменными (A, Y*, B)и (b, g) над переменными (B, Y**, C) пара утверждений (a, g)спецификацией над переменными (A, Y***, C) при некоторых Y*,Y**, Y***? Зависит ли ответ от выбора указанных множествпеременных?181.3 Задача верификацииЧастичная и полная корректность программПусть программа задана своей моделью в виде блок-схемы P, аее спецификация  – предикатами  и . Мы будем говорить, что• программа P частично корректна относительно  и , еслидля любого вектора значений входных переменных х, такогочто (х) = Т и M[P](х)  , выполнено ограничение (х, M[P](х))=Т. Частичную корректность программы P относительно и  мы будем обозначать {}P{}.• программа P полностью корректна относительно  и , еслидля любого вектора значений входных переменных х, такогочто (х) = Т, выполнены ограничения M[P] (х)   и (х,M[P](х))=Т.ПолнуюкорректностьпрограммыPотносительно  и  мы будем обозначать P.Заметим, что полная корректность программы P относительновходного предиката и выходного предиката T эквивалентнатому, что программа P завершается всегда, когда вектор значенийвходных переменных удовлетворяет .

В этом случае мы будемговорить, что P завершается на . Напомним, что это означает, чтосоответствующее вычисление заканчивается в одном из операторовHALT со значениями всех переменных не равными .Лемма 2. Пусть даны программа P и спецификация  = ( , ). В этом случае P тогда и только тогда, когда {}P{} иPT.19Исходяизданнойлеммы,длядоказательстваполнойкорректности программы необходимо и достаточно доказать еечастичную корректность и завершаемость.Из определения корректности также следует, что и частичная, иполная корректность сохраняется при замене входного предикатана более сильный и выходного на более слабый.