gds

coq + imperative algorithm proving

Aug 14, 2013 18:28

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины ( Read more... )

Leave a comment

Comments 12

plumqqz August 14 2013, 15:57:03 UTC
Если не секрет, зачем тесты, если есть доказательства? Ну или наоборот...

Reply

gds August 14 2013, 16:07:39 UTC
тесты -- затем, чтобы проверить, правильную ли я модель накодил для доказательств. Ну да всё равно тестировал производительность, там и корректность заодно проверил.

Если бы меня не попросили проверить, есть ли смысл в "умной буферизации" по производительности, я бы не лепил тесты, проверил бы потом, в деле.

А наоборот -- если есть тесты, полные, исправляемые при каждом изменении функциональности, то доказательства не нужны. Если же исправлять их лень, или нет гарантий полноты тестов, то есть смысл подумать о доказательствах.

Reply

plumqqz August 14 2013, 16:14:39 UTC
Если же исправлять их лень, или нет гарантий полноты тестов, то есть смысл подумать о доказательствах.
Да, но может же ведь быть ошибка и в модели, которая, как обычно, будет именно в том месте, для которого было лень переделывать тесты?

Reply

gds August 14 2013, 16:34:58 UTC
1. в моделях ошибок обычно сильно меньше.
2. в случае доказательств я уверен: как бы ни менялся код, доказательства будут постоянно отражать факты о коде. В случае тестов таких гарантий никто не даст, там надо морочиться с test coverage всяким.

Reply


ex_juan_gan August 14 2013, 16:10:26 UTC
wow

Reply


nivanych August 15 2013, 03:36:23 UTC
Юзерпик хороший.
Кажется мне, что ты как-то слишком сложно делаешь.
Нутром это чую, но доказать не могу (c)

Reply

gds August 15 2013, 09:37:18 UTC
давай идеи, будем упрощать.

Reply

nivanych August 15 2013, 14:15:35 UTC
А йа даже посмотрел.
Ладно. Сойдёмся на том, что сложность состоит в разнице мышления между нами ;-)

Reply

gds August 15 2013, 14:51:05 UTC
ну хорошо, как бы ты подошёл к решению этой задачи (а именно, "реализовать и доказать императивный алгоритм")? Свести его к потоку блоков -- не очень-то вариант. Ещё идеи?

Reply


thedeemon August 15 2013, 08:20:06 UTC
Сперва поразился числу строк, а потом смотрю - там каждый аргумент на отдельной строке. Зачем так?

В целом прикольно, вспомнился ATS, где любой ввод-вывод практически в такую вот штуку выливается, и встроенный решатель целочисленный как раз на такие задачки хорошо заточен. Только, не зная кока, складывается впечатление, что это все write-only, и что никто кроме автора (и тот лишь в интервале сегодня - две недели спустя) в этом не разберется.

Reply

gds August 15 2013, 09:46:05 UTC
да, в некоторых местах можно было бы и в одну строку записать. А так -- в случаях, когда предметная область не близка, я предпочитаю предельную структурированность и ясность кода, чтобы связь выравнивания и ast была как можно более явной. А текущая задача была пока не близкой мне.

Про "не разберётся" -- разберётся ещё как. В типах, сигнатурах и телах функций уж точно. А пруфы -- так, хуйня из-под коня, в которой разбираться особо не нужно. А в окамловском коде разбираться и не нужно -- это всего лишь результат трансляции.

Reply


Leave a comment

Up