Каждая рассматриваемая нами Zonnon-программа реализует некоторую функцию, отображающую множество значений входного файла в множестве значений выходного файла, сопоставляет каждому элементу из области определения функции в точности один элемент из области значений. Поэтому любой "хороший" способ определения реализуемой функции может использоваться в качестве внешней спецификации программы. Рассмотрим небольшой пример.
Пусть имеется задача нахождения максимального из двух натуральных чисел. Внешняя ее спецификация может быть представлена следующим образом:
Программа: Максимальное из двух натуральных чисел
Вход:
где
Integer,
Integer,
,
Выход:
где L=Макс(N,M)
Здесь первая строчка (раздел "Программа") содержит название программы.
Вторая строчка (раздел "Вход") -- это обозначения для содержимого входного
файла в начальном состоянии вычисления, а третья (раздел "где") -- это
набор утверждений, описывающих допустимое множество входных данных (допустимы
те и только те наборы значений, на которых утверждения принимают истинное
значение). Четвертая строчка (раздел "Выход") содержит обозначение содержимого
выходного файла в заключительном состоянии вычисления, а пятая и последующие
(второй раздел "где") описывают функциональную связь результата программы
с ее аргументом. Для записи утверждений и функциональной связи используется
язык математики, в том числе системы функциональных равенств (см. п. 1.1.3),
а также понятия и конструкции, присутствующие в языке Zonnon. В спецификации
ясно и точно указано, что областью определения функции, реализуемой программой,
является множество всех пар неотрицательных чисел
и
,
а также то, что программа должна печатать значение
,
если
,
и M, если N < M.
Заметим, что способ, использованный нами для определения функции ,
является достаточно удобным и наглядным. Вместе с тем, при таком задании
область определения функции (множество тех объектов, которые можно подставлять
вместо параметров определения; для определения функции
параметрами являются
и
)
и область ее значений даны неявно и не всегда очевидны. То, что функции
предполагаются в качестве аргументов произвольные пары неотрицательных
целых чисел, выражается в дополнительных ограничениях, а тот факт, что
областью значений в этом случае является множество неотрицательных целых
чисел, хотя и выводится из правила получения результата функции, тем не
менее не выражен явно. Фактически можно считать, что рассмотренное правило
задает функцию
с существенно более широкими областями определения и значений. Например,
в нем явно задано, как получить максимальное из любых двух целых или вещественных
чисел. Более точно, правило получения значения функции Макс(N,M) определено
для любых таких объектов N
и M, для которых определены операции "
"
и "
".
Рассмотрим другой пример. Пусть требуется найти наибольшее из трех вещественных чисел, т.е. требуется построить программу, удовлетворяющую следующей спецификации:
Программа: Наибольшее из трех вещественных чисел
Вход:
где
Выход:
где S=Наиб(N,M,K)
Наиб(x,y,z)=Макс(x,Макс(y,z)),
В общем случае спецификация программы может включать целую систему определений
функций, каждое из которых является равенством
или имеет вид
где ,
,
-- переменные, называемые параметрами определения,
-- выражения одного и того же типа (это тип результата определяемой функции
),
а
-- логические выражения. Предполагается, что выражения
,
строятся из констант и переменных
применением к ним имеющихся в языке операций и стандартных функций, а также
функций, определяемых с помощью данной системы определений.
Как уже отмечалось в п. 1.1.3, правила нахождения для конкретных значений
c
значения функции
,
заданной такими определениями, предполагают подстановку значений
вместо параметров
в выражения
и нахождение их значений. Если ни одно из логических выражений
не принимает после подстановки истинного значения, то значение
не определено. Если же для некоторого
есть выражение E
,
принимающее значение true, то в качестве значения
берется значение выражения, полученного из
подстановкой
вместо
.
Нахождение значения некоторого выражения B(например,
или
)
осуществляется по шагам, на каждом из которых в B
рассматривается первое слева подвыражение B
,
содержащее только одно применение операции или функции, и делается замена
B
,
либо на его значение, если B
не содержит определяемых функций, либо на то подвыражение B
,
значение которого определяет значение выражения B
в соответствии с определением функции, образующей B
.
Таким образом, внешняя спецификация рассмотренного вида по существу является программой на языке математических определений, процесс выполнения которой -- это преобразование формул с помощью подстановок.
Следует иметь в виду, что при пошаговой разработке программ качество
результирующей программы во многом определяется тем, как мы определим ее
внешнюю спецификацию. Рассмотрим две разные спецификации задачи возведения
вещественного числа
в десятую степень.
Программа: Возведение в десятую степень
Вход: A
где
Выход:
где
,
.
Программа: Быстрое возведение в десятую степень
Вход: A
где A
Выход:
где
,
.
Первая спецификация задает процесс преобразований выражений, который
соответствует вычислениям по программе X10
(см. п. 2.2.6), в то время, как вторая описывает идею, лежащую в основе
более эффективных программ X10A, X10B, X10C (например, для числа 2 получается
следующая последовательность выражений:
B
= Степ
=
=
=
=
=
.
Next:2.3.3
Утверждения как множества Up:2.3
Доказательство свойств программ
Previous:2.3.1
Зачем нужны доказательства