w
Кстати, немного офтопик, но тем не менее.
А как часто такие алгоритмы как мой пытаются формально верифицировать?
Стоит ли такое вообще пытаться верифицировать?
Size: a a a
2021 April 13
AG
это в общем-то одно из ключевых направлений в верификации и есть
AT
Новая работа? Эх...
AS
Нее… Работа старая, отношение новое ))
Я ж на курс “Введение в верификацию” записался. Поэтому вот эти вопросы начали появляться.
Я ж на курс “Введение в верификацию” записался. Поэтому вот эти вопросы начали появляться.
R
С рафтом прикольная история. Его на тла описали, потом тла запрувили и нашли ошипки
AS
Чот такое слышал.
Но мой случай точно проще.
Но мой случай точно проще.
R
Ну ето алекс сюда кидал))
AG
ну если брать ручную верификацию, то там вылазит всё та же проблема с отсутствием канонических теорий - непонятно как задавать спецификацию
AG
поэтому такого рода штуки обычно долбят автоматизированными методами типа модел чекеров
AS
Пока она у меня в виде UML seq диаграммы 😅
AG
собственно сам Антон этим и занимается :)
AS
Я думал, что он над криптом и умнодоговорами
AG
да, это последнее поколение дист-систем :)
AG
леджеры и надстройки над ними
AG
консенсус через игровые методы
AS
Эх вот зря я так и не осилил TLA+ PlusCal
AG
я тоже по секрету говоря ;)
AS
Ну это принципиально другой уровень сложности.
Моя проблема - это как сортировка пузырьком по сравнению с mergesort
Моя проблема - это как сортировка пузырьком по сравнению с mergesort
AG
ну там просто свои задачи