ATS: какие ваши доказательства?

Nov 26, 2011 20:55

В прошлой серии мы увидели, как зависимые типы в ATS помогают избежать грубых ошибок вроде выхода за пределы строки или массива. А можно ли продвинуться еще дальше в деле обеспечения корректности? Можно ли полностью доказать статически, что функция делает ровно то, что надо, и всегда выдает верный результат? В ряде случаев можно. В ATS мы можем ( Read more... )

ats, fp

Leave a comment

Comments 6

udpn November 26 2011, 20:41:02 UTC

... )

Reply


boltatel November 26 2011, 22:12:43 UTC
Похоже на смесь Паскаля с Прологом.

Reply

thedeemon November 27 2011, 04:54:11 UTC
В пролог заложена процедура поиска, а тут надо вручную конструктивно доказательства строить. Ну а паскаль тут может напоминать разве что указание типа после переменной, но это для функциональных языков традиционно и, кажется, появилось еще до паскаля.

Reply


xeno_by November 27 2011, 09:32:05 UTC
В прошлом посте было написано, что на отсутствие эффектов указывает :<> (а из возможных эффектов мы видели только cloref0). Здесь упоминаются такие замечательные функции как malloc_gc и fgets_err, причем у них в сигнатуре написано :<>. Как это? Какие вообще эффекты могут трекаться атсом?

Reply

thedeemon November 27 2011, 11:37:16 UTC
Эффектов отслеживается три: exn (исключения), ntm (незавершимость) и ref (изменение общей памяти). Помимо эффектов в тех же угловых скобках может быть указан вид функции - fun (простая), cloref (замыкание в управляемой куче), cloptr (замыкание в освобождаемой вручную памяти), prf (функция-доказательство) и lin (одноразовая функция). Также есть сокращения: 0 - без эффектов, 1 - с любыми эффектами.
I/O эффектом не считается, и это действительно довольно странно.

Reply


rigidus November 27 2011, 22:07:15 UTC
Это прямо как репортаж из будущего. С нетерпением жду продолжения

Reply


Leave a comment

Up