Структурное программирование Неудобные ситуации в программировании Гиперфункция и оператор продолжения ветвей Свойства гиперфункций Правила доказательства. - презентация

1 Структурное программирование Неудобные ситуации в программировании Гиперфункция и оператор продолжения ветвей Свойства гиперфункций Правила доказательства корректности гиперфункций Пример. Вычисление суммы чисел в строке Пример. Решение системы линейных уравнений Лекция 8 Предикатное программирование

2 7. Технология предикатного программирования 7.4. Гиперфункции

3 Структурное программирование Эдвард Дейкстра begin ; end if then else end while do end

4 type SEQ(int p, q) = array p..q of T; int n; //номер последнего элемента списка SEQ(0, n) K;... if (n 0) return ; T b = K[1]; for (int i = 1; ;) { T a = K[i - 1]; for (int j = i; ; j = j – 1) { if (a b) { K[j] = b; break} elseif (j = 1) { K[0] = b; K[1] = a; break } else{ K[j] = a; a = K[j - 2] } } if (i = n) break else{ i = i + 1; b = K[i] } } b = K[i] ….. a b для a = K[i - 1] K[j] = b избыточный

5 Неудобные ситуации elemTwo(list(int) s: int e, bool exists ) {if (s = nil s.cdr = nil) exsts = false else { e = s.cdr.car || exists = true } } post exists = (s nil & s.cdr nil) & (exists e = s.cdr.car) elemTwo(s: e, exists); if (exists) B(e…) else D(…) (7.13) if ( s = nil s.cdr = nil ) (7.14) { exist = false; if (exist) B(e…) else D(…) } else {{e = s.cdr.car || exist = true }; if (exist) B(e…) else D(…)} if (s = nil s.cdr = nil) D(…) else { e = s.cdr.car; B(e…) }

6 P(x) { A(x: y, z) } Q(x, y, z), x, y и z возможно пустые Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) Предикаты S(x, y) и R(x, z) функции S: x y и R: x z. C(x) истинно Q(x, y, z) совпадает с S: x y C(x) ложно Q(x, y, z) совпадает с R: x z. Q(x, y, z) результат склеивания функций S: x y и R: x z. В Q(x, y, z) не определено значение набора z, если C(x) истинно. Аналогично, не определено значение y при ложном C(x). Лемма Если предикат S(x, y) тотален в области P(x) & C(x), а R(x, z) в области P(x) & C(x), то спецификация предиката A(x: y, z) является тотальной. Лемма Если предикат S(x, y) является однозначным в области P(x) & C(x), а R(x, z) в области P(x) & C(x), то спецификация предиката A(x: y, z) является однозначной.

7 P(x) { A(x: y, z) } Q(x, y, z) Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) Пусть вызов A используется во фрагменте вида: A(x: y, z); if (C(x)) B(y: u) else D(z: u) (7.17) Вычисление C(x) может оказаться трудоемким. Очевидно, что значение C(x) можно вычислить внутри определения предиката A. Введем логическую переменную c и следующим образом инструментируем определение предиката A, превратив его в A(x: c, y, z). Если некоторая ветвь тела предиката A завершается присваиванием набору y, то в конце этой ветви вставляется оператор c = true; если ветвь завершается вычислением z, то в конце ее вставляется c = false. Тогда фрагмент (7.17) можно заменить более эффективным: A(x: c, y, z); if (c) B(y: u) else D(z: u) (7.18)

8 Пример. Решение системы линейных уравнений type VEC(nat k) = array (real, 1..k); type MATRICE(nat k) = array(real, 1..k, 1..k); Lin (nat n, MATRICE(n) a, VEC(n) b: VEC(n) x) pre det(n, a) 0 // > post LinEq(n, a, x, b); Иногда требуется решить более общую задачу: Lin1(nat n, MATRICE(n) a, VEC(n) b: bool c; VEC(n) x) post c = (det(n, a) 0) & (c LinEq(n, a, x, b)); Lin1(n, a, b: c; x); if (c) B(x…) else D(…) LinEq(a, x, b)

9 P(x) { A(x: y, z) } Q(x, y, z) Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) A(x: y, z); if (C(x)) B(y: u) else D(z: u) (7.17) A(x: c, y, z); if (c) B(y: u) else D(z: u) (7.18) Рассмотрим подстановку определения A на место вызова в (7.18) с последующим упрощением. Обнаруживается, что втягивание условного оператора внутрь подставленного тела A может привести к появлению нескольких копий вызовов B(y…) и D(z…). Применим другое преобразование. Альтернативы условного оператора пометим метками 1 и 2. Получим оператор: if (c) 1: B(y: u) else 2: D(z: u) (7.19) Далее в подставленном теле A всякий оператор c = true заменим на #1, а c = false на #2. Операторы #1 и #2 операторы goto 1 и goto 2. Например: if ( s = nil s.cdr = nil ) #2 else { e = s.cdr.car; #1 }; if (exist) 1: B(e…) else 2: D(…)

10 Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) A(x: y, z); if (C(x)) B(y: u) else D(z: u) (7.17) A(x: c, y, z); if (c) B(y: u) else D(z: u) (7.18) if (c) 1: B(y: u) else 2: D(z: u) (7.19) Модифицированный фрагмент (7.18) запишем в виде: A(x: y, z); if (c) 1: B(y: u) else 2: D(z: u) (7.20) A блок, результат подстановки определения A и замены c = true и c = false на #1 и #2. Заменим оператор (7.19) последовательностью: 1: B(y: u); goto 3; 2: D(z: u); 3: (7.21) Композицию вида (7.21) запишем в следующем виде: case 1: B(y: u) case 2: D(z: u) (7.22) case 1: B(y: u) и case 2: D(z: u) операторы продолжения ветви, а вместе обработчик ветвей. Обработчику ветвей предшествует оператор, содержащий операторы перехода. Если предшествующий оператор нормально завершается (не оператором перехода), то обработчик ветвей пропускается.

11 A(x: y, z); if (C(x)) B(y: u) else D(z: u) (7.17) A(x: c, y, z); if (c) B(y: u) else D(z: u) (7.18) if (c) 1: B(y: u) else 2: D(z: u) (7.19) A(x: y, z); if (c) 1: B(y: u) else 2: D(z: u) (7.20) 1: B(y: u); goto 3; 2: D(z: u); 3: (7.21) case 1: B(y: u) case 2: D(z: u) (7.22) Отметим, что оператор (7.19) эквивалентен: if (c) #1 else #2; case 1: B(y: u) case 2: D(z: u) (7.23) Отметим также, что блок A(x: y, z) эквивалентен композиции: A(x: c, y, z); if (c) #1 else #2 (7.24) В итоге, исходный фрагмент (7.17) эквивалентен: A(x: y, z) case 1: B(y: u) case 2: D(z: u) (7.25) Исходный предикат A(x: y, z) будем записывать в виде A(x: y #1: z #2) и называть гиперфункцией с двумя ветвями. Метки 1 и 2 являются метками ветвей.

12 P(x) { A(x: y, z) } Q(x, y, z) Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) A(x: y, z); if (C(x)) B(y: u) else D(z: u) (7.17) case 1: B(y: u) case 2: D(z: u) (7.22) A(x: y, z); case 1: B(y: u) case 2: D(z: u) (7.25) Определение гиперфункции : A(x: y #1: z #2) pre P(x); pre 1: C(x) (7.26) { A(x: y, z) } post 1: S(x, y); post 2: R(x, z); Блок A(x: y, z) тело гиперфункции, P(x) общее предусловие, C(x) предусловие первой ветви гиперфункции, S(x, y) постусловие первой ветви, R(x, z) постусловие второй ветви. Фрагмент (7.17) записывается следующим образом: A(x: y #1: z #2) case 1: B(y: u) case 2: D(z: u) (7.27) Для композиции (7.27) допускается более компактная запись: A(x: y : z) case B(y: u) case D(z: u) (7.28)

13 elemTwo(list (int) s : int e : ) pre 1: s nil & s.cdr nil {if (s = nil s.cdr = nil) #2 else { e = s.cdr.car #1 } } post 1: e = s.cdr.car; elemTwo(list (int) s : int e #1 : #2) elemTwo(s: e: ) case B(e…) case D(…) elemTwo B(e…) D(…)

14 A(x: y #1: z #2) pre P(x); pre 1: C(x) (7.26) { A(x: y, z) } post 1: S(x, y); post 2: R(x, z); V(x, u) pre P V (x) { A(x: y : z) case B(y: u) case D(z: u) } post Q V (x, u); (7.29) P(x) { A(x: y, z) } Q(x, y, z), {P B (y)} B {Q B (y, u)}, {P D (z)} D {Q D (z, u)}, Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) V(x, u) pre P V (x) {A(x: y, z); if (C(x)) B(y: u) else D(z: u)} post Q V (x, u);(7.30) H(x, y, z, u) pre P H (x, y, z ){if (C(x)) B(y: u) else D(z: u)} post Q H (x, y, z, u) Получим формулы для предусловия и постусловия предиката H: P H (x, y, z ) (C(x) P B (y)) ( C(x) P D (z)) Q H (x, y, z, u) (C(x) Q B (y, u)) ( C(x) Q D (z, u)) Определение (7.30) эквивалентно следующему: V(x, u) pre P V (x) {A(x: y, z); H(x, y, z, u)} post Q V (x, u); (7.31) Построим правила RS1 и RS2 для суперпозиции в определении (7.31): Правило RS1. P V (x) P(x) y,z (Q(x, y, z) P H (x, y, z )) Правило RS2. P V (x) & y,z (Q(x, y, z) & Q H (x, y, z, u)) Q V (x, u) Далее подставим формулы для Q, P H и Q H. Получим правила: Правило RS1. P V (x) P(x) y,z((C(x) S(x, y)) ( C(x) R(x, z)) (C(x) P B (y)) ( C(x) P D (z))) Правило RS2. P V (x) & y,z ((C(x) S(x, y)) ( C(x) R(x, z)) & (C(x) Q B (y, u)) ( C(x) Q D (z, u))) Q V (x, u) Специализация по C(x)

15 A(x: y #1: z #2) pre P(x); pre 1: C(x) (7.26) { A(x: y, z) } post 1: S(x, y); post 2: R(x, z); V(x, u) pre P V (x) { A(x: y : z) case B(y: u) case D(z: u) } post Q V (x, u); (7.29) P(x) { A(x: y, z) } Q(x, y, z), {P B (y)} B {Q B (y, u)}, {P D (z)} D {Q D (z, u)}, Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) Правило RS9. P V (x) P(x) Правило RS10. P V (x) C(x) y (S(x, y) P B (y)) Правило RS11. P V (x) C(x) z (R(x, z) P D (z)) Правило RS12. P V (x) C(x) & y (S(x, y) & Q B (y, u)) Q V (x, u) Правило RS13. P V (x) C(x) & z (R(x, z) & Q D (z, u)) Q V (x, u) В итоге, справедлива следующая лемма: Лемма Пусть предусловие P V (x) истинно. Допустим, предикаты A, B и D корректны. Если правила RS9 RS13 истинны, то предикат V, представленный определением (7.29) является корректным.

16 A(x: y #1: z #2) pre P(x); pre 1: C(x) (7.26) { A(x: y, z) } post 1: S(x, y); post 2: R(x, z); V(x, u) pre P V (x) { A(x: y : z) case B(y: u) case D(z: u) } post Q V (x, u); (7.29) P(x) { A(x: y, z) } Q(x, y, z), {P B (y)} B {Q B (y, u)}, {P D (z)} D {Q D (z, u)}, Q(x, y, z) (C(x) S(x, y)) ( C(x) R(x, z)) (7.16) Правила серии L для (7.29) Для (7.31) построим правила LS1 и LS2: Правило LS1. P V (x) P(x) Правило LS2. P V (x) & Q V (x, u) & Q(x, y, z) P H (x, y, z) & Q H (x, y, z, u) Для правила LS2 подставим формулы для Q, P H и Q H. Получим: Правило LS2. P V (x) & Q V (x, u) & (C(x) S(x, y)) ( C(x) R(x, z)) (C(x) P B (y)) ( C(x) P D (z)) & (C(x) Q B (y, u)) ( C(x) Q D (z, u)) Специализация по условию C(x) дает следующие правила: Правило LS10. P V (x) P(x) Правило LS11. P V (x) & Q V (x, u) & C(x) & S(x, y) P B (y) & Q B (y, u) Правило LS12. P V (x) & Q V (x, u) & C(x) R(x, z) P D (z) & Q D (z, u) Лемма Допустим, спецификация предиката V реализуема, предикаты A, B и D однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS10, LS11 и LS12 истинны, то предикат V, представленный определением (7.29) является корректным.

17 Пример 7.4. Определим гиперфункцию Comp следующей спецификацией: Comp(list (int) s: : int d, list (int) r) pre 1: s = nil post 2: d = s.car & r = s.cdr; Построим определение предиката elemTwo через гиперфункцию Comp без полей car, cdr и конструктора nil. elemTwo(list (int) s: int e #1: #2) pre 1: s != nil & s.cdr != nil {int e1; list (int) s1, s2; Comp(s: : e1, s1) case #2 case { Comp(s1: : e, s2) case #2 case #1 } } post 1: e = s.cdr.car;

18 Если оператор продолжения ветви содержит только оператор перехода, то оператор перехода переносится в конец соответствующей ветви вызова гиперфункции. elemTwo(list (int) s: int e #1: #2) pre 1: s != nil & s.cdr != nil {Comp(s: #2: int e1, list (int) s1) case Comp(s1: #2: e, list(int) s2 #1); } post 1: e = s.cdr.car; Реализован перенос описаний локальных переменных e1, s1 и s2 в позиции их определения. Если обработчик ветвей состоит из единственного оператора продолжения ветви, а предшествующий оператор не имеет нормального завершения исполнения, то обработчик ветвей вырождается. В этом случае оператор продолжения ветви устраняется, а находящийся в нем оператор композируется с предыдущим оператором в виде оператора суперпозиции. elemTwo(list (int) s: int e #1: #2) pre 1: s != nil & s.cdr != nil {Comp(s: #2: _, list (int) s1); Comp(s1: #2: e, _ #1); } post 1: e = s.cdr.car ; Вхождения локальных переменных e1 и s2 заменены стандартным именем _, означающим, что результат игнорируется при исполнении.

19 Гиперфункция и оператор продолжения ветвей H(x: y : z) (C(x) P(x, y)) ( C(x) Q(x, z)) H(x: y : z) case R(y: …) case S(z: …) x y z H R S C(x) dom(H) H(x: Y y, Z z) (C(x) P(x, y)) ( C(x) Q(x, z)) ветвь гиперфункции

20 if ( (x)) H(x…: … : …) { A; B } case B else { C; D } case D H(X x…: … : …) { if ( (x)) {A #1} else {C #2} } Свойства гиперфункций

21 Пример. Сумма чисел в строке СуммаСтроки(string s: nat n) post P(s, n); Предикат P(s, n) определяется рекурсивным образом. цифра(char c) c {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; число(string s) s nil & s1,s2 string c char (s = s1 + c + s2 цифра(c)) val(string s: nat n) pre число(s) post n значение числа s. P(string s, nat n) (s = nil n = 0) & & (число(s) n = val(s)) & ( s1 string c char. цифра(c) & s = c + s1 P(s1, n)) & & ( s1,s2 string c char. цифра(c) & число(s1) & s = s1 + c + s2 m. P(s2, m) & n = val(s1) + m) string есть list(char), а + обозначает конкатенацию строк. Лемма Спецификация предиката СуммаСтроки тотальна.

22 Обобщение исходной задачи : Сумма(string s, nat m: nat n) post x. P(s, x) & n = m + x; Ввиду истинности СуммаСтроки(s: n) Сумма(s, 0: n) корректно следующее определение предиката: СуммаСтроки(string s: nat n) {Сумма(s, 0: n)} post P(s, n); Алгоритм: Находится первая цифра. Вычисляется число, начинающееся с этой цифры. Для оставшейся части строки действие алгоритма повторяется. При нахождении первой цифры возможна ситуация, когда строка не содержит цифр. Данную ситуацию обозначим предикатом: мусор(string s) s1,s2 string c char (s = s1 + c + s2 цифра(c)) В частности, предикат истинен для пустой строки. Определение первой цифры выражается гиперфункцией: перваяЦифра(string s: : char e, string r) pre 1: мусор(s) post 2: w. мусор(w) & s = w + e + r & цифра(e); Лемма Спецификация гиперфункции перваяЦифра тотальна.

23 Отметим, что можно было бы использовать гиперфункцию вида: перваяЦифра1(string s: : string r), где r начинается с первой цифры, однако в реализации это приведет к повторному доступу к одной и той же литере в строке. В практике типично решение: перваяЦифра2(string s: char e, string r) Здесь отсутствие цифр в строке s кодируется некоторым значением e, отличным от цифры. Вред подобных трюков обычно проявляется для сложных программ. Решение в виде гиперфункции дает более короткую и эффективную программу. Вторая часть алгоритма выделение числа в строке и его вычисление представляется предикатом: числоВстроке(char e, string r: nat v, string t) pre цифра(e) post w. конецЧисла(r, w, t) & v = val(e + w); конецЧисла(r, w, t) r = w + t & (w = nil число(w)) & (t = nil цифра(t.car); Лемма Спецификация предиката числоВстроке тотальна.

24 Сумма(string s, nat m : nat n) {перваяЦифра(s: : char e, string r) case n = m case {числоВстроке(e, r: nat v, string t); Сумма(t, m + v: n)} } post x. P(s, x) & n = m + x measure len(s); A(x: y, z); if (C(x)) B(x, y: u) else D(x, z: u)(7.17) Правило FG1.R(x, u) P(x) Правило FG2.R(x, u) & С(x) & S(x, y) LS(B(x, y: u)) Правило FG3.R(x, u) & С(x) & G(x, z) LS(D(x, z: u)) FG2 : lemma Q_Сумма(s,m,n) & P1_ перваяЦифра(s) => n = m; FG3: Q_Сумма(s,m,n) & not P1_ перваяЦифра(s) & Q2_ перваяЦифра(s,e,r) LS(числоВстроке(e, r: nat v, string t); Сумма(t, m + v: n)) Правило FS5.R(x, y) P(x) правила для суперпозиции Правило FS6.R(x, y) & Q(x, z) LS(B(x, z: y)) FS6 : Q_Сумма(s,m,n) & Q2_ перваяЦифра(s,e,r) & Q_ числоВстроке(e,r,v, t) LS(Сумма(t, m + v: n)) числоВстроке(char e, string r: nat v, string t) pre цифра(e) post w. конецЧисла(r, w, t) & v = val(e + w); конецЧисла(r, w, t) r = w + t & (w = nil число(w)) & (t = nil цифра(t.car); перваяЦифра(string s: : char e, string r) pre 1: мусор(s) post 2: w. мусор(w) & s = w + e + r & цифра(e);

25 перваяЦифра(string s: : char e, string r) pre 1: мусор(s) { switch (s) { case nil: #1 case cons(a, u): if (цифра(a)) { r = u || e = a #2} else перваяЦифра(u: #1 : e, r #2) } } post 2: w. мусор(w) & s = w + e + r & цифра(e) measure len(s); Это эквивалентно: if (s = nil) P1_перваяЦифра(s) else if (цифра(s.car)) { r = s.cdr || e = s.car || мусор(s) } else { перваяЦифра(s.cdr : : e, r ) || !!! if (мусор(s.cdr)) мусор(s) else мусор(s) } Q_перваяЦифра(s, e, r) = мусор(s) or Q2_перваяЦифра(s, e, r) пЦ: lemma Q_перваяЦифра(s, e, r) => s = nil ? мусор(s) : цифра(s.car) ? r = s.cdr & e = s.car & мусор(s) : len(s.cdr) < len(s) & Q_перваяЦифра(s.cdr, e, r) & ( мусор(s.cdr)? мусор(s) : мусор(s) )

26 Чтобы получить хвостовую рекурсию для предиката числоВстроке необходимо ввести накопитель для вычисления значения очередного числа. Определим предикат: взятьЧисло(string r, nat p: nat v, string t) post w. конецЧисла(r, w, t) & val1(w, p, v); val(s: n) pre число(s) post val1(s, 0, n); formula val1(stringw, nat p, n) = w = nil ? n = p : val1(w.cdr, p 10 + valD(w.car), n) где valD(e) значение цифры e. Тогда корректно следующее определение предиката: числоВстроке(char e, string r: nat v, string t) pre цифра(e) { взятьЧисло(r, val(e): v, t) } post w. конецЧисла(r, w, t) & v = val(e + w); конецЧисла(r, w, t) r = w + t & (w = nil число(w)) & (t = nil цифра(t.car);

27 взятьЧисло(string r, nat p: nat v, string t) { if (r = nil) {v = p || t = r} else {{char b = r.car || string q = r.cdr}; if (цифра(b)) взятьЧисло(q, p 10 + val(b): v, t) else {v = p || t = q} } } post w. конецЧисла(r, w, t) & val1(w, p, v) measure len(r); Доказательство. Пусть истинно постусловие взятьЧисло. Докажем истинность тела. Пусть истинно условие r = nil. Тогда w = nil и t = nil. Далее, v = p. Это доказывает истинность оператора v = p || t = r. Пусть истинно условие r nil. Докажем истинность второй альтернативы внешнего условного оператора. Истинны предусловия операций car и cdr. Далее достаточно доказать истинность внутреннего условного оператора при b = r.car и q = r.cdr. Тогда r = b + q. Пусть истинно условие цифра(b). Докажем истинность рекурсивного вызова. Поскольку len(q) < len(r), то рекурсивный вызов можно заменить его постусловием: h. конецЧисла(q, h, t) & val1(h, p 10 + val(b), v) (7.37) Докажем истинность (7.37). Поскольку r = b + q и цифра(b), то w = b + h для некоторого h и истинно конецЧисла(q, h, t). Из определения val1 при r nil следует, что val1(w, p, v) val1(h, p 10 + val(b), v). В итоге, истинна формула (7.37). конецЧисла(r, w, t) r = w + t & (w = nil число(w)) & (t = nil цифра(t.car);

28 Сумма: n m; s r, t; Склеивания перваяЦифра: s r, u; e a; числоВстроке: s r, t;замена на s для упрощения взятьЧисло: s r, q, t; v p; СуммаСтроки(string s: nat n){Сумма(s, 0: n)}; Сумма(string s, nat n : nat n) {перваяЦифра(s: : char e, string s) case n = n case {числоВстроке(e, s: nat v, string s); Сумма(s, n + v: n)} } перваяЦифра(string s: : char e, string s) { switch (s) { case nil: #1 case cons(e, s): if (цифра(e)) { s = s || e = e #2} else перваяЦифра(s: #1 : e, s #2) }

29 числоВстроке(char e, string s: nat v, string s) { взятьЧисло(s, val(e): v, s) } взятьЧисло(string s, nat v: nat v, string s) { if (s = nil) {v = v || s = s} else {{char b = s.car || s = s.cdr }; if (цифра(b)) взятьЧисло(s, v 10 + val(b): v, s) else {v = v || s = s} } }; Замена хвостовой рекурсии циклом. Удаляются операторы вида n = n. Удаляется оператор продолжения case n = n СуммаСтроки(string s: nat n){Сумма(s, 0: n)}; Сумма(string s, nat n : nat n) {for (; ;) { перваяЦифра(s: #M1 : char e, string s #2) case 2:{числоВстроке(e, s: nat v, string s); n = n + v} } M1: }

30 перваяЦифра(string s: #1 : char e, string s #2) {for (; ;) { switch (s) { case nil: #1 case cons(e, s): if (цифра(e)) #2 else {} } числоВстроке(char e, string s: nat v, string s) { взятьЧисло(s, val(e): v, s) } взятьЧисло(string s, nat v: nat v, string s) {for (; ;) { if (s = nil) break else {{char b = s.car || s = s.cdr}; if (цифра(b)) v = v 10 + val(b) else break } };

31 Подставим определения предикатов взятьЧисло и перваяЦифра на место вызовов. Проведем очевидные упрощения. Сумма(string s, nat n : nat n) {for (; ;) { for (; ;) { switch (s) { case nil: #M1 case cons(char e, s): if (цифра(e)) #2 } case 2:{числоВстроке(e, s: nat v, string s); n= n + v} } M1: } числоВстроке(char e, string s: nat v, string s) { v = val(e); for (; ;) { if (s = nil) break {char b = s.car || s = s.cdr}; if (цифра(b)) v = v 10 + val(b) else break } };

32 Поскольку внутренний цикл в теле предиката Сумма не имеет нормального выхода, можно заменить оператор #2 на break и убрать скобки оператора продолжения ветви. Подставим определение числоВстроке на место вызова, а затем определение предиката Сумма в тело СуммаСтроки. СуммаСтроки(string s: nat n) (7.38) {n = 0; for (; ;) { if (s = nil) return { char e = s.car || s = s.cdr }; if (цифра(e)) break } nat v = val(e); for (; ;) { if (s = nil) break {char b = s.car || s = s.cdr }; if (цифра(b)) v = v 10 + val(b) else break } n = n + v }

33 Кодирование последовательностей Необходимо кодировать начальное значение строки s и текущее. Начальное состояние вырезка S[m..p], текущее S[j..p]. Массив S и величины j, m, p должны быть определены в программе, причем j переменная, а m и p могут быть константами. type STR = array (char, M..N); STR S; int j = m; Значения границ M и N должны быть достаточными, т.е. M m, p, j N. Операции с последовательностью s кодируются следующим образом: s = nil j > p s.car S[j] s = s.cdr j = j + 1

34 type STR = array (char, M..N);(7.39) STR S; nat n = 0; for (int j = m; ;) { for (; ;) { if (j > p) return char e = S[j]; j = j + 1; if (цифра(e)) break } nat v = val(e); for (;j

35 Имеется недостаток программы (7.39): если строка s завершается цифрой, то проверка исчерпания строки реализуется дважды. Чтобы исправить недостаток, следует вместо предиката числоВстроке(e, r: v, t) использовать гиперфункцию числоВстроке1(e, r: v1: v2, t), в которой первая ветвь реализуется при исчерпании входной строки r. Возможен другой более простой алгоритм. На очередном шаге вычисляется значение очередного числа в строке в виде предиката числоВстроке(s: v, t), где v значение очередного числа, а t остаток непустой строки s. Если первый элемент s не является цифрой, то v = 0. Реализация данного алгоритма дает более короткую программу, чем (7.39), однако менее эффективную. По сравнению с (7.39) лишними действиями являются операторы v = 0 и n = n + v для каждого символа, отличного от цифры.

36 int n=0, j=0; while (j < N) { e=S[j++]; w = 0; while (j < N && String.IsNumber(e)) { w = int.Parse(e) + w * 10; e = S[j++]; } n = n + w; }