Геймеры доказали свою пользу для верификации ПО

Могут ли весёлые игры в онлайне решить сложные проблемы с верификацией программного обеспечения, которыми обычно занимаются профессиональные эксперты в программировании? Другими словами, будет ли армия необразованных геймеров лучше, чем профессиональный процесс? Исследователи из Агентства по перспективным оборонным научно-исследовательским разработкам США (DARPA) уверены, что так и есть.

Первые эксперименты показали, что краудсорсинг даже эффективнее, чем предполагалось. Программа под названием Краудсорсинговая формальная верификация (Crowd Sourced Formal Verification, CSFV) началась в декабре 2013 года, и тогда открыли портал Verigames с пятью бесплатными играми на онлайновую верификацию.

Например, на скриншоте вверху изображена игра Paradox, в которой нужно устранить конфликты, изменяя состояние экранных переменных. По достижении установленного результата перед игроком ставят новую задачу на оптимизацию.

Кроме Paradox, есть ещё космическая головоломка Dynamakr для складывания паззла из космического генератора паттернов; битва с инопланетными захватчиками Ghost Map Hyperspaceс целью украсть их расщелины (через которые гады пересекают ткань пространства-времени) и путешествие по средневековой земле монстров Monster Proof с попутным решением головоломок ради обогащения.



В последней пятой игре Binary Fission нужно отсортировать атомные частицы в минимально возможное количество шагов.



На прошлой неделе DARPA объявило об успехе первого этапа программы и вскоре добавить ещё пять игр на сайт.

Из сообщения в блоге DARPA: «Эти [2013] игры транслировали действия игроков в аннотации к программам и помогли экспертам по формальной верификации в создании математических доказательств, которые подтверждают отсутствие важных классов ошибок в языках программирования C и Java. Первоначальный анализ показывает, что дилетанты, которые играли в игры CSFV, создали тысячи тысяч аннотаций».

В общем, геймерский проект оказался очень удачным.

Пожалуй, не следует беспокоиться из-за неизбежно высокого уровня безработицы в роботизированном обществе будущего. Программисты всегда предложат людям интересные и полезные занятия.

Источник: geektimes.ru/post/251402/