программы-спецификации, или как философия обманывает
Я думаю, вы слышали утверждение, что в хорошем языке программирования программы являются спецификациями. Мол, к этому мы все должны стремиться. Почему, собственно, программы должны быть спецификациями? Если программа отличается от спецификации, тогда надо доказать, что программа удовлетворяет спецификации, то есть верифицировать эту программу. А верификация - это кака (при обосновании этого утверждения могут ссылаться на Гёделя). Если программа есть спецификация, то ничего доказывать не надо (утверждение 0). Круто!
Рассмотрим простой пример. Заказана функция, которая возвращает наименьший элемент списка. Список содержит только числа. Наименьший элемент списка - это такой элемент, который принадлежит этому списку и меньше всех элементов этого списка (используя математический термин, есть нижняя грань (lower bound) этого списка). Это спецификация. Для реализации этой функции я возьму язык программирования Пролог, в котором, как все мы знаем, программы есть спецификации. Наша спецификация почти буквально превращается в программу-спецификацию 0.
lb_list(_, []).
lb_list(X, [Y|L]) :- X =< Y, lb_list(X, L).
min_list_spec(X, L) :- member(X, L), lb_list(X, L).
lb_list(X, L) - X меньше всех элементов L. Но кое-что портит всю малину: min_list_spec занимает O(n^2) времени. Даже самый невежественный программист знает, как решить эту задачу за O(n) времени. Например, так (программа-спецификация 1).
min(X, Y, X) :- X =< Y.
min(X, Y, Y) :- X > Y.
min_list_prg(X, [X]).
min_list_prg(R0, [X|L]) :- min_list_prg(R1, L), min(X, R1, R0).
Итак, имеем 2 программы-спецификации; я лично не вижу очевидного способа преобразовать одну в другую. Программа-спецификация 1 более эффективна, а программа-спецификация 0 более близка к нашему пониманию задачи. Таким образом, программа-спецификация 1 больше похожа на программу, а программа-спецификация 0 больше похожа на спецификацию. Что же, не удалось обмануть природу.
Этот пример демонстрирует вредность философии. Утверждение 0 выглядит истинным, но, если посмотреть на него с другой стороны, выглядит ложным. :-) Это потому, что утверждение 0 философское. Поскольку в философии нет точных определений, философские выводы сомнительны. Слава Богу, в математике подобная фигня не возможна. Философия, как интуиция, помогает открывать что-то новое, и ещё она помогает открывать что-то ложное.
Рассмотрим простой пример. Заказана функция, которая возвращает наименьший элемент списка. Список содержит только числа. Наименьший элемент списка - это такой элемент, который принадлежит этому списку и меньше всех элементов этого списка (используя математический термин, есть нижняя грань (lower bound) этого списка). Это спецификация. Для реализации этой функции я возьму язык программирования Пролог, в котором, как все мы знаем, программы есть спецификации. Наша спецификация почти буквально превращается в программу-спецификацию 0.
lb_list(_, []).
lb_list(X, [Y|L]) :- X =< Y, lb_list(X, L).
min_list_spec(X, L) :- member(X, L), lb_list(X, L).
lb_list(X, L) - X меньше всех элементов L. Но кое-что портит всю малину: min_list_spec занимает O(n^2) времени. Даже самый невежественный программист знает, как решить эту задачу за O(n) времени. Например, так (программа-спецификация 1).
min(X, Y, X) :- X =< Y.
min(X, Y, Y) :- X > Y.
min_list_prg(X, [X]).
min_list_prg(R0, [X|L]) :- min_list_prg(R1, L), min(X, R1, R0).
Итак, имеем 2 программы-спецификации; я лично не вижу очевидного способа преобразовать одну в другую. Программа-спецификация 1 более эффективна, а программа-спецификация 0 более близка к нашему пониманию задачи. Таким образом, программа-спецификация 1 больше похожа на программу, а программа-спецификация 0 больше похожа на спецификацию. Что же, не удалось обмануть природу.
Этот пример демонстрирует вредность философии. Утверждение 0 выглядит истинным, но, если посмотреть на него с другой стороны, выглядит ложным. :-) Это потому, что утверждение 0 философское. Поскольку в философии нет точных определений, философские выводы сомнительны. Слава Богу, в математике подобная фигня не возможна. Философия, как интуиция, помогает открывать что-то новое, и ещё она помогает открывать что-то ложное.