Существуют ли аннотированные системы формальной проверки для чисто функциональных языков программирования?

25

ACSL (Ansi C Specification Language) - это спецификация для кода C, снабженная специальными комментариями, которая позволяет формально проверять код C.

Я не рассматривал это, но я полагаю, что формальные методы, используемые в верификаторах ACSL , будут похожи на Hoare Logic. Однако для чисто функциональных языков, таких как Haskell, я не представляю, какой формализм будет использоваться для формальной проверки.

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

Я знаю, что есть зависимая типизация, которую поддерживают многие языки (Agda, Idris и т. Д.), Но в Хаскель-зависимой типизации сложно без некоторого (нечитаемого?) Волшебства типов. Имея это в виду, и поскольку Haskell имеет гораздо лучшую библиотечную поддержку, чем Agda и Idris, я считаю, что такая система для функциональной формальной проверки может быть полезной, но я не знаю, проводилось ли исследование по этому вопросу или нет.

Натан Беделл
источник

Ответы:

13

Хонда и Йошида

(вероятно) впервые применил логику Хоара для чисто функциональных языков. Эта работа основана на логике Хеннесси-Милнера и кодировании функций Милнером в процессы, как описано здесь:

Работа Régis-Gianas и др., Упомянутая в другом ответе, аналогична первой работе Honda / Yoshida выше. Это было распространено на эффективные языки в стиле ML:

Упомянутая логика - это то, что называется наблюдательно полной, это означает, что операционная и логическая семантика совпадают. Артур Шарже использовал эту полноту для своей работы по проверке функциональных программ в стиле Хоара в Coq.

Мартин Бергер
источник
15

F*

Кажется, существует тесное соответствие между типами уточнения и ACSL-подобными обозначениями.

Наконец, я могу только предложить поближе взглянуть на Agda и Idris, поскольку они могут компилироваться в Haskell и направлены на то, чтобы предоставить пользователю удобный язык программирования (особенно Idris). Я подозреваю, что можно без особых проблем интегрировать библиотеки Haskell в код Idris.

Коди
источник
без особых проблем - не совсем. Идрис строг по умолчанию, а Хаскель ленив; это само по себе создает серьезную проблему. Совместимость с Haskell также никогда не была приоритетом для дизайна Idris.
Бартек Банахевич
Справедливо. Agda проверяет завершение по умолчанию, поэтому такие вещи, как строгость, не являются проблемой в теории . Конечно, время выполнения может сильно отличаться.
Коди
11

См. Также кандидатскую диссертацию Янна Режиса-Джанаса с Франсуа Поттье: логика Хоара для функциональных программ по вызову по стоимости (MPC'08) . Эта работа была расширена, чтобы охватить обычные побочные эффекты ML, предложенные Йоханнесом Канигом и Джин-Кристофом Филлиатром в 2009 году: Кто: проверяющий эффект для программ высшего порядка .

gasche
источник
8

В этом году в ICFP есть статья , уточняющая типы для Haskell . В статье рассматривается проверка завершения, а не полная логика Хоара, но, надеюсь, это начало в этом направлении.

Соответствующий раздел работы в этой статье содержит некоторые указатели, такие как статическая проверка контрактов Сюэса, Пейтон-Джонса и Клэссена на Haskell , и Sonnex, Drossopoulou, а также Zeno и Vytiniotis Эйзенбаха, Пейтон-Джонса, Claessen и Halo Розена .

Охад Каммар
источник
1

Наша работа по мягкой проверке контрактов связана с OOPSLA 2012 и ICFP 2014 и позволяет вам писать контракты, которые очень похожи на спецификации ACSL, а затем либо статически проверять их, либо использовать их динамические проверки во время выполнения.

Сэм Тобин-Хохштадт
источник