Интересно. Я тоже думал, что там доказательное программирование, а не тесты.
Кстати, а что это за штука такая? Вот как, например, доказательно запрограммировать вычисление факториала на Прологе? Насколько я помню, писать такие вещи на Прологе - одно удовольствие, ибо не нужно никаких циклов, проверок условий и т.п., а просто тупо пишем определение факториала, и всё.
Но вот незадача: Если аргумент достаточно большой (далеко до упоминавшегося ранее миллиарда), то программа вылетает даже не по переполнению основного регистра, а по банальному stack overfow, ибо на деле выполняется рекурсивный вызов одной и той же простой подпрограммы. Вот как мы должны так "доказательно программировать", чтобы пользователь в ответ на ввод аргумента получал всегда разумные ответы, т.е., например, "Введённое число слишком большое", а не "Переполнение стека в строке 5678 модуля fig.ego.znaet.gde"?
