ACSL (Ansi C Specification Language) - это спецификация для кода C, снабженная специальными комментариями, которая позволяет формально проверять код C.
Я не рассматривал это, но я полагаю, что формальные методы, используемые в верификаторах ACSL , будут похожи на Hoare Logic. Однако для чисто функциональных языков, таких как Haskell, я не представляю, какой формализм будет использоваться для формальной проверки.
Кто-нибудь сделал что-то похожее на ACSL , но для чисто функционального языка? Если нет, проводилось ли какое-либо исследование формальной проверки аннотируемого стиля для функциональных языков?
Я знаю, что есть зависимая типизация, которую поддерживают многие языки (Agda, Idris и т. Д.), Но в Хаскель-зависимой типизации сложно без некоторого (нечитаемого?) Волшебства типов. Имея это в виду, и поскольку Haskell имеет гораздо лучшую библиотечную поддержку, чем Agda и Idris, я считаю, что такая система для функциональной формальной проверки может быть полезной, но я не знаю, проводилось ли исследование по этому вопросу или нет.
См. Также кандидатскую диссертацию Янна Режиса-Джанаса с Франсуа Поттье: логика Хоара для функциональных программ по вызову по стоимости (MPC'08) . Эта работа была расширена, чтобы охватить обычные побочные эффекты ML, предложенные Йоханнесом Канигом и Джин-Кристофом Филлиатром в 2009 году: Кто: проверяющий эффект для программ высшего порядка .
источник
В этом году в ICFP есть статья , уточняющая типы для Haskell . В статье рассматривается проверка завершения, а не полная логика Хоара, но, надеюсь, это начало в этом направлении.
Соответствующий раздел работы в этой статье содержит некоторые указатели, такие как статическая проверка контрактов Сюэса, Пейтон-Джонса и Клэссена на Haskell , и Sonnex, Drossopoulou, а также Zeno и Vytiniotis Эйзенбаха, Пейтон-Джонса, Claessen и Halo Розена .
источник
Наша работа по мягкой проверке контрактов связана с OOPSLA 2012 и ICFP 2014 и позволяет вам писать контракты, которые очень похожи на спецификации ACSL, а затем либо статически проверять их, либо использовать их динамические проверки во время выполнения.
источник