Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ. Можно лишь показать что ПО 100% работоспособно на ограниченном мн-ве тестов. Кто-то из них неправ