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

При решениизадачи необходимо (явно или неявно) составить модель этойфункциивповторятьмоделируявидетекстблок-схемы.функцииБлок-схемабезпоследовательностьпоследовательностьюдолжнадословнопреобразованиявыражений,операторовфункциисоответствующихподсхем,условныйоператор и операторы цикла – при помощи соответствующихоператоров языка блок-схем. Все локальные переменные функцииобъявляются в её начале и моделируются соответствующимоператоромSTART.Дляупрощениясчитать,чтовсеарифметические операции выполняются точно, разрядной сеткихватает для проведения всех необходимых вычислений в этойфункции.1.4.1 В блок-схеме на рисунке 5 заданы путь  и предикат p1:Dx  Dy  {Т, F} – на значения входных и промежуточныхпеременных в начале этого пути.42START(y1, y2) ← (0, 0)CAFBy1 = xTDHALTz ← y2(y1 , y2) ← (y1 + 1, y2 + x)Рисунок 5.

Рисунок к задачеЗаписать точный предикат p2: Dx  Dy  {Т, F} – на значениявходных и промежуточных переменных в конце этого пути, есливычисление идет по пути значениямивходныхи начинается из конфигурации соипромежуточныхпеременных,удовлетворяющими предикату p1.Т.е. записать предикат p2 истинный на тех и только техзначениях x'  Dx и y'  Dy, для которых существуют x  Dx и y Dy такие, что выполнено p1(x, y), и существует вычисление,начинающееся в конфигурации со значениями переменных (x, y),выполняющееся по пути  и завершающееся в конфигурации вконце пути со значениями переменных (x', y'). Множествопеременных V = {x, y1, y2, z} состоит из одной входной, двухпромежуточных и одной выходной переменной.

Доменами всехпеременных является множество целых чисел.a) : B – C; p1(x, y1, y2) = (x = 0 ∧ y1 = 0 ∧ y2 = 1)b) : B – C; p1(x, y1, y2) = (y2 = 1)43c) : B – C; p1(x, y1, y2) = (y1 = x)d) : B – C; p1(x, y1, y2) = (1 < y1 < 10 ∧ y2 > x)e) : B – C – B; p1(x, y1, y2) = (y1·x = y2)f) : B – C – B – C – B; p1(x, y1, y2) = (y1·x = y2)g) : C – B – C; p1(x, y1, y2) = (y1·x = y2)h) : C – B – C; p1(x, y1, y2) = (y2 < 0)i) : A – B – C – A; p1(x, y1, y2) = (y1 ≥ x)j) : B – C – D; p1(x, y1, y2) = (y1 = 1 ∧ y2 = 0)k) : B – C – D; p1(x, y1, y2) = (y1 = 1)l) : START – A – B – C – B – C – A – D – HALT; p1(x, y1, y2) =(x = 2 ∧ 0 ≤ y1 < x)1.4.2 Для заданной блок-схемы, спецификации, точек сечения,индуктивныхутверждений,фундированногомножестваиоценочных функций выпишите все те и только те условияверификации, корректности и завершимости, которые не являютсяистинными при доказательстве полной корректности блок-схемыотносительноспецификацииприпомощиметодовФлойда.Доменами всех переменных является множество всех целых чисел.a) φ(x) = (x > 0)START(y1, y2) ← (0, x)AFψ(x, z) = (z > 0)pA(x, y1, y2) = (y1 ≤ 2y2)W = (Nat0, <)y1 ← y1 + 1y1 < 2y2FTy1 < y2TuA(x, y1, y2) = y1HALTz ← y2 - y144b) φ(x) = (|x| < 10)START(y1, y2) ← (0, x)ψ(x, z) = (|x| = |z|)pA(x, y1, y2) = (y1 = -x)y1 ← y1 - y2pB(x, y1, y2) = (y1 = -x)CpC(x, y1, y2) = (y2 = x ∧ x > 0)TW = (Nat0, <)y1 < 0A Fy1 ≥ 1uB(x, y1, y2) = y1 – 1FuA(x, y1, y2) = y1HALTz ← y2 - y1uC(x, y1, y2) = y1c) φ(x) = (x > 0)ψ(x, z) = (z ≥ x)pA(x, y1, y2) = (y1 = x)W = (Nat0, <)uA(x, y1, y2) = y2START(y1, y2) ← (x, x)Ty1 < y2ATy1 < y2Fy1 ← 0FHALTz ← y1 + y245BTd) φ(x) = (|x| < 5)START(y1, y2) ← (x, 0)ψ(x, z) = (z ≥ 0)pA(x, y1, y2) = (y1 = -x)TCpB(x, y1, y2) = (y1 = -x)A(y2 = x ∧ x > 0)W = (Nat0, <)HALTz ← y1 - y2y2 ← y1 + y2pC(x, y1, y2) =FFy1 < y2By1 > 0TuB(x, y1, y2) = y1 – 1uA(x, y1, y2) = y1uC(x, y1, y2) = y1START(y1, y2) ← (3x, x)e) φ(x) = (x ≥ 0)ψ(x, z) = (z > 0)pA(x, y1, y2) = (y2 = x)FpB(x, y1, y2) = (y2 = x)FApC(x, y1, y2) = (y2 = x ∧ y1 ≥ 0)W = (Nat0, <)uA(x, y1, y2) = y1 + 2y1 > 2y2Ty1 = y2 + 1THALTz ← y1 + y2uB(x, y1, y2) = y1uC(x, y1, y2) = y1 + 1C3 | y1F46BTf) φ(x) = (x ≥ 0)ψ(x, z) = (|z| = x)pA(x, y1, y2) = (y2 = x ∧ y1 = 0)pB(x, y1, y2) = (y2 = 0  y1 = 0)W = (Nat0, <)pC(x, y1, y2) = (2y1 = y2 + x)uC(x, y1, y2) = y2 – 1uA(x, y1, y2) = y2uB(x, y1, y2) = y2 + 1START(y1, y2) ← (0, x)F Ay1 < y2CTB Ty1 + y2 < 0T2y1 = y2+ xFHALTz ← y1 + y2F1.4.3 При помощи метода индуктивных утверждений доказать,что следующаяблок-схемачастичнокорректнаотносительноуказанной спецификации (φ, ψ).

Доменом каждой переменнойявляется множество всех целых чисел.Спецификация: φ(x) = Tψ(x, z) = (z = 2x)START(y1, y2) ← (0, 1)Fy1 = x(y1, y2) ← (y1 + 1, y2 + y2)47THALTz ← y21.4.4 При помощи метода индуктивных утверждений доказать,что следующаяблок-схемачастичнокорректнаотносительноуказанной спецификации (φ, ψ). Доменом каждой переменнойявляется множество всех целых чисел.START(y1, y2, y3) ← (1 + x1 + x2, 1, x1 + x2)FTy3 = x1(y1, y2) ← (y1 + y3, 1 + y2 + y3)HALT(z1, z2) ← (y1 - y3, x2 + 2y2 - y1)y3 ← y3 - 1Спецификация:φ(x1, x2) = (x2 ≥ 0)ψ(x1, x2, z1, z2) = (z1 - x1 = z2 – x2)1.4.5 При помощи метода индуктивных утверждений доказать,что следующаяуказаннойблок-схемаспецификациичастично(φ,ψ),корректнадоменомявляется множество всех целых чисел:φ(x) = (x ≥ 0)ψ(x, z) = (z2 ≤ x < (z + 1)2)START(y1, y2, y3) ← (0, 0, 1)y2 ← y2 + y3FTy2 > xHALTz ← y1(y1, y3) ← (y1 + 1, y3 + 2)48всехотносительнопеременных1.4.6 Следующая функция языка Си была промоделированауказанной ниже блок-схемой.

В блок-схеме выделена точка сеченияА, которой приписано утверждение p(x, y1, y2) = (0 ≤ y1 < x). Обоснуйте или опровергните следующее утверждение: p выполнено всякий раз, когда вычисление находится в точке А (т. е. может бытьиспользовано для доказательства частичной корректности). Функция вызывается только с положительными значениями х.int sum(int x){int i = 0, s = 0;for(; i < x; i++){s += i;}return s;}START(y1, y2) ← (0, 0)TAy1 < xy2 ← y2 + y1FHALTz ← y2y1 ← y1 + 1491.4.7 Обоснованно ответить на вопрос: какое требуется минимальное число точек сечения, чтобы доказать частичную корректность хотя бы одной блок-схемы, имеющей указанные особенности,относительно хотя бы одной спецификации при помощи методовФлойда, если блок-схемы с указанными особенностями существуют.Если ответ зависит от спецификации, привести не менее двухразных ответов и обосновать их.a) блок-схема содержит 2 цикла;b) блок-схема содержит не менее одного оператора соединения;c) блок-схема зацикливается на всех значениях входных данныхиз своих доменов;d) операторы и связки блок-схемы разбиваются на 3 независимые связные части так, что первая и вторая часть обладаютединственной общей связкой, вторая и третья часть обладаютединственной общей связкой, а первая и третья часть не обладают общими связками.

Общих операторов у частей нет.1.4.8 Обоснованно ответить на вопрос: какое требуется минимальное число точек сечения, чтобы доказать завершаемость хотябы одной блок-схемы, имеющей указанные особенности, относительно хотя бы одной спецификации при помощи методов Флойда,если блок-схемы с указанными особенностями существуют. Еслиответ зависит от спецификации, привести не менее двух разных ответов и обосновать их. Если доказать завершаемость невозможно,обоснуйте это.a) блок-схема содержит 2 цикла;b) блок-схема содержит не менее одного оператора соединения;50c) блок-схема зацикливается на всех значениях входных данныхиз своих доменов;d) операторы и связки блок-схемы разбиваются на 3 независимые связные части так, что первая и вторая часть обладаютединственной общей связкой, вторая и третья часть обладаютединственной общей связкой, а первая и третья часть не обладают общими связками. Общих операторов у частей нет.1.4.9 Дановыражение.Обосноватьилиопровергнутьутверждение: существует блок-схема P, спецификация (, ψ) длянее и доказательство Pψ при помощи методов Флойда, вкотором данное выражение используется в качестве оценочнойфункции.a) x (x – целое число);b) x2 (x – целое число);c) sin2 x + cos2 x (x – вещественное число);d) 1 / x (x – вещественное число);e) x (x – очередь из целых чисел);f) x (x – очередь из неотрицательных целых чисел).1.4.10 Каковоминимальноеимаксимальноечислоутверждений, которые необходимо доказать при использованиилишь одной точки сечения в рамках доказательства частичнойкорректности P (она задана в виде программой на языке Си)?полной корректности?Ответ обосновать.

Если одной точки сечения недостаточно,обосновать это. Напишите, как зависит ответ от спецификацииэтой блок-схемы.51a) int P(int x) {int y1 = x, y2 = x;do {if (y1 > y2 + y2) {y2 ++;}y1 += y2;} while (y1 < y2);return y1 + y2;}b) int P(int x1, int x2) {int y1 = x1, y2 = x2;while (x1 > y1) {switch (y1 + y2) {case 0: y1 ++;case 1: y2 ++;}return -1;}return y1 + y2;}c) int P(int x1, int x2) {int y1 = x1, y2 = x2, y3 = 0;while (y3 < x) {if (y1 < y2)return y3;y1 = y2 = y3;52}while (y2 > 0) {if (y1 < 2 * y3)break;y2 --;}return 0;}d) char *strcpy(char *dest, const char *src) {char *p = dest, *q = src;while (*q != 0) {*p = *q;q++;}return dest;}1.4.11 Можно ли только при помощи методов Флойда доказать,что в указанной функции на языке Си значение указанной переменной всегда принадлежит указанному множеству значений? Еслида, покажите, как (предъявив хотя бы несколько формальных выкладок).

Если нет, обоснуйте это. Если спецификация не указана,считается, что она содержит тождественно истинные предусловие ипостусловие. Если в этой функции указанная переменная не всегдапринадлежит указанному множеству значений, обоснуйте это.a) void swap(int *x, int *y) {int t = *x;*x = *y;53*y = t;}переменная: x, область значений: не-0 указатели.b) int abs(int *x) {int y = -1;if (x != 0 && (y = *x) < 0) {*x = - y;return *x;}return -1;}переменная: y, область значений: отрицательныечисла; предусловие: x != 0.c) int search(int x, int *data, size_t len) {int i = 0;for ( ; i < len; i++) {if (data[i] == x) return i;}return -1;}переменная: i, область значений: 0 <= i < len;предусловие: data указывает на массив размера неменее len.541.4.12 Можно ли только при помощи методов Флойда доказать,что в приведенной ниже функции на языке Си никогда не выполняется указанное условие на значения переменных? Если да, покажите, как (предъявив хотя бы несколько формальных выкладок).Если нет, обоснуйте это.