- Проверка типов для языка программирования логики с ограничениями на основе наборов (arXiv)
Автор:Максимилиано Кристиа, Джанфранко Росси
Аннотация:{log} (читается как «setlog») — это язык логического программирования с ограничениями (CLP) и решатель выполнимости, областью ограничений которого является теория конечных множеств. Основанный на CLP и Прологе, {log} по существу предоставляет нетипизированный язык. Таким образом, он может принимать формулы, которые заставляют решатель производить нежелательное поведение. Кроме того, пользователи {log} могут делать ошибки в своих программах, которые обычно обнаруживаются программой проверки типов. В частности, {log} был предложен в качестве языка прототипирования для спецификаций B и Z, которые являются типизированными формализмами. Кроме того, без системы типов для {log} возникает пробел, который пользователям необходимо заполнять вручную. Поэтому в этой статье мы определяем систему типов и реализуем проверку типов для {log}. Доказано, что система типов безопасна (надежна) путем адаптации формулировки безопасности типов функционального программирования к контексту CLP. Мы также покажем, как можно комбинировать типы и CLP, чтобы обеспечить более надежную гарантию правильности программы. Наконец, мы применяем систему типов, средство проверки типов и их комбинацию с CLP к реальному кейсу из авиационной области.
2.Отмена императивного параллельного языка программирования (arXiv)
Автор:Джеймс Хоуи, Ирек Улидовски
Аннотация: мы представляем метод реверсирования выполнения императивных параллельных программ. Для необратимой программы мы описываем процесс создания двух версий. Первый выполняет прямое исполнение и сохраняет информацию, необходимую для реверсирования. Второй использует эту сохраненную информацию для имитации разворота. Мы предлагаем использовать идентификаторы для преодоления проблем реверсирования параллельных программ. Мы доказываем правильность этой обратимости, показывая, что исходное состояние программы восстанавливается и вся сохраненная информация используется (без мусора).
3.Обзор моделей глубокого обучения для структурного понимания кода (arXiv)
Автор: Руотин Ву, Юсинь Чжан, Цибиао Пэн, Лян Чен, Цзыбин Чжэн
Аннотация. В последние годы рост требований к глубокому обучению и автоматизации в индустрии программного обеспечения поднял интеллектуальную разработку программного обеспечения на новую высоту. Количество подходов и приложений к пониманию кода растет, и во многих из них используются методы глубокого обучения для лучшего захвата информации в данных кода. В этом обзоре мы представляем всесторонний обзор структур, сформированных из кодовых данных. Мы разделяем модели понимания кода последних лет на две группы: модели на основе последовательностей и модели на основе графов, далее делаем их обобщение и сравнение1. Мы также представляем метрики, наборы данных и последующие задачи. Наконец, мы вносим некоторые предложения для будущих исследований в области понимания структурного кода.
4.Giallar: проверка по нажатию кнопки для квантового компилятора Qiskit(arXiv)
Автор: Жуньчжоу Тао, Юньонг Ши, Цзянан Яо, Сюпэн Ли, Али Джавади-Абхари, Эндрю В. Кросс, Фредерик Т. Чонг, Рунхуэй Гу
Аннотация: в этой статье представлен Giallar, полностью автоматизированный инструментарий проверки для квантовых компиляторов. Giallar не требует ручных спецификаций, инвариантов или доказательств и может автоматически проверять, что проход компилятора сохраняет семантику квантовых схем. Для работы с неограниченными циклами в квантовых компиляторах Джаллар абстрагирует три шаблона циклов, инварианты циклов которых можно вывести автоматически. Чтобы эффективно проверять эквивалентность произвольных входных и выходных схем, которые имеют сложное представление матричной семантики, Джаллар вводит символическое представление для квантовых схем и набор правил перезаписи для демонстрации эквивалентности символических квантовых схем. С Giallar мы реализовали и проверили 44 (из 56) проходов компилятора в 13 версиях компилятора Qiskit, стандарта квантового компилятора с открытым исходным кодом, во время которых Qiskit обнаружила и подтвердила три ошибки. Наша оценка показывает, что большинство проходов компилятора Qiskit могут быть автоматически проверены за считанные секунды, а проверка накладывает лишь скромные накладные расходы на производительность компиляции.
5.Односортные программные алгебры(arXiv)
Автор:Игорь Седлар, Иоганн Й. Ванненбург
Аннотация:Алгебра Клини с тестами, KAT, обеспечивает простую двухсортную алгебраическую основу для проверки свойств пропозициональных программ while. Алгебра Клини с доменом, KAD, является односортной альтернативой KAT. Эквациональная теория КАТ встраивается в КАД, но в КАД отсутствуют некоторые естественные свойства КАТ. Например, не каждая алгебра Клини расширяется до KAD, и подалгебра тестов в каждой KAD вынуждена быть максимальной булевой подалгеброй отрицательного конуса. В этой статье мы предлагаем обобщение KAD, которое избегает этих особенностей, но при этом включает эквациональную теорию KAT. Мы показываем, что некоторые естественные свойства оператора области определения KAD могут быть добавлены к обобщенной структуре, не влияя на результаты. Мы рассматриваем вариант схемы, в которой тестовое дополнение определяется с помощью невязки умножения алгебры Клини.
