else break

}

n = n + v

}

Можно обнаружить следующий недостаток программы (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 для каждого символа, отличного от цифры.

Заключение

Технология предикатного программирования предоставляет аппарат для доказательства корректности предикатных программ. При наличии спецификации в виде предусловия и постусловия для каждого определяемого предиката корректность предикатной программы может быть доказана строго математически. Используемая техника доказательства базируется на системе правил доказательства корректности для конструкций языка P. Здесь демонстрировалась техника, соответствующая правилам серии L для однозначных программ и спецификаций. Это техника доказательства в стиле синтеза программы. Логика, применяемая в процессе доказательства, аналогична той, которую обычно использует программист при построении программы. Процесс доказательства хорошо структурирован и даже для большой программы состоит из небольших независимых частей, что предопределяет возможность успешной автоматизации доказательства корректности предикатных программ.

Язык предикатного программирования позволяет писать программы в естественной логике и при этом обладает гораздо большей выразительностью в сравнении с языками императивного программирования. На языке предикатного программирования можно записать любой алгоритм (для задач с предикатной спецификацией), который представим на императивном языке. Аппарат гиперфункций предоставляет новые возможности адекватного и эффективного представления алгоритма. Гиперфункциям нет аналогов в императивных языках. Эффективность в предикатном программировании обеспечивается применением серии оптимизирующих трансформаций. В результате получается императивная программа, которая по эффективности не хуже написанной вручную и почти всегда короче.

Список литература

1. Мир Лиспа. Методы и системы программирования: Пер. с англ. М.: Мир, 1990. Т. 2. 318 с.

2. Ершов А. П. Введение в теоретическое программирование. М.: Наука, 1977. 288 с.

3. Поттосин И. В. Направленные преобразования линейного участка // Языки и системы программирования. Новосибирск, 1981. С. 14-28. (Сб./ВЦ СО АН СССР).

4. Bacon D., Graham S., Sharp O. Compiler transformations for high-performance computing // ACM Computing surveys. 1994. Vol. 26. No. 4. P. 345-420.

5. Петров Э. Ю. Склеивание переменных в предикатной программе // Методы предикатного программирования. Новосибирск, 2003. С. 48-61.

6. Кнут Д. Искусство программирования для ЭВМ. Сортировка и поиск: Пер. с англ. М.: Мир, 1978. Т.3. 843 с.

7. Шелехов В. И., Карнаухов Н. С. Демонстрация технологии предикатного программирования на задаче сортировки простыми вставками // Методы предикатного программирования. Новосибирск, 2003. С. 16-21.

[1] Первые программы писала математик Ада Лавлейс, дочь поэта лорда Байрона, для спроектированной, но не реализованной вычислительной машины Чарльза Беббиджа в 1830-х гг.

[2] Здесь и далее имеется в виду исчисление предикатов высших порядков.

[3] К статической семантике относятся правила идентификации переменных и других объектов программы, совокупность ограничений для значений атрибутов конструкций и система умолчаний.

[4] CCP - Calculus of Computable Predicates.

[5] Практически все языки функционального программирования содержат расширения, включающие конструкции императивного программирования в целях повышения эффективности программ. Такие языки не являются чистыми.

[6] Родственным, но не совпадающим является понятие слабейшего предусловия, введенное Э. Дейкстра [1]; E. Hehner использует термин «точное предусловие» для уточнения [15].

[7] Данная тройка совпадает с (2.5).

[8] Данная тройка совпадает с (2.11).

[9] Эта тройка совпадает с (2.12).

[10] Эта тройка совпадает с (2.13).

[11] Предикат b(t) может оказаться истинным для других элементов t, не являющихся минимальными.

[12] Термов в смысле языка исчисления предикатов

[13] Размеченное объединение в терминологии Т. Хоара [2].

[14] Здесь и далее параметром функции LS является произвольная языковая конструкция. Запись функции LS отличается от используемой в гл. 2.

[15] Если H - переменная предикатного типа, то будем считать, что H входит в набор x.

[16] Чтобы не загромождать пример, используется оператор суперпозиции более общего вида по сравнению с (4.18).

[17] Не обеспечивается даже монотонность для Øb & (x, y) Î Q.

[18] Здесь и далее используется иная форма записи тройки Хоара по сравнению с {P(x)} S {Q(x, y)} в гл. 2.

[19] На самом деле однозначность проверять не требуется, однако для неоднозначной спецификации будет невозможно доказать истинность правил RR3 и RR4.

[20] Ввиду возможной погрешности обычно используют условие det(a) > e с константой e, близкой к нулю.