На самом деле есть. Существует форма спецификации для функциональных языков, основанная на абстрактных типах данных, называемая алгебраической спецификацией. Их поведение в некоторых отношениях очень похоже на поведение объектов, однако конструкции логичны и математичны и неизменны, как функциональные конструкции.
В конкретном языке функциональной спецификации, который используется в классе Algorithms и Data Structures в Университете Буэнос-Айреса, есть генераторы, наблюдатели и дополнительные операции.
Генератор - это выражение, которое является одновременно экземпляром и возможной композицией типа данных.
Например, для двоичного дерева (ADT bt) у нас есть нулевые узлы и двоичные узлы. Таким образом, у нас были бы генераторы:
-nil
-bin(left:bt, root: a, right:bt)
Где left - это экземпляр bt, корень - это общее значение, а right - еще один bt.
Таким образом, nil является допустимой формой bt, но bin (bin (nil, 1, nil), 2, nil) также допустим, представляя двоичное дерево с корневым узлом со значением 2, левый дочерний узел с значение 1 и нулевой дочерний правый узел.
Таким образом, для функции, которая скажет, вычисляет количество узлов в дереве, вы определяете наблюдателя ADT и определяете набор аксиом, которые отображаются на каждый генератор.
Так, например:
numberOfNodes(nil) == 0
numberOfNodes(bin(left,x,right))== 1 + numberOfNodes(left) + numberOfNodes(right)
Это имеет преимущество использования рекурсивных определений операций и обладает более формально интересным свойством, что вы можете использовать то, что называется структурной индукцией, чтобы ДОКАЗАТЬ, что ваша спецификация верна (да, вы демонстрируете, что ваш алгоритм будет давать правильный результат ).
Это довольно академическая тема, редко встречающаяся за пределами академических кругов, но она того стоит, чтобы получить представление о разработке программы, которая может изменить ваши взгляды на алгоритмы и структуры данных.
Правильная библиография включает в себя:
Берно Г., Бидоит М. и Кнапик Т.
1995. Спецификации наблюдений и предположение о неразличимости.
Теор. Вычи. Sci. 139, 1-2 (март.
1995), 275-314. DOI =
http://dx.doi.org/10.1016/0304-3975(94)00017-D
Гуттаг, Дж. В. и Хорнинг, Дж. Дж. 1993.
Лиственница: языки и инструменты для формального
Спецификация. Springer-Verlag Новый
Йорк, Inc. Абстракция и
Спецификация в разработке программного обеспечения,
Барбара Лисков и Джон Гуттаг, MIT
Press, 1986.
Основы алгебраики
Спецификация 1. Уравнения и начальные
Семантика. H. Ehrig y B. Mahr
Springer-Verlag, Берлин, Гейдельберг,
Нью-Йорк, Токио, Германия, 1985.
С соответствующими ссылками:
http://www.cs.st -andrews.ac.uk / ~ сослагательного наклонения / Ресурсы / Notes / FormalSpec / AlgebraicSpec.pdf
http://nms.lcs.mit.edu/larch/pub/larchBook.ps
Это чертовски интересная тема.