Кто занимается Coq в SPb?
Alexander Vlasov
Возник вопрос - занимается ли кто в Питере такими вещами как Coq и
прочее (Type Theory, Higher Order Logics, Proof assistants,
verification etc)?
Я думал я один такой, но на SPbHUG видел, что был доклад Евгения
Кирпичева по Coq оказывается, так что я знаю что не один :).
Меня идея верификации с детства (точнее лет с 18ти прикалывала), а
сейчас этим можно реально заниматься, и есть уже серьезные проекты
(типа верифицированных компиляторов и ядер ОС).
Не скажу что я эксперт, но Coq вчерне освоил (dependent types, Ltac),
в планах сделать сертифицированный компилятор ПХП: есть некоторые идеи
по оптимизации скриптовых языков.
Также есть наметки по верификации Джава с использованием Coq, но это
планы совсем на будущее.
Если кто подобными вещами занимается (или кто знает, что кто-то
занимается), напишите здесь плиз - интересно знать, насколько эта тема
представлена в Питере.
Спасибо,
Власов Александр
Denis Moskvin
<glav...@gmail.com> написал:
> Привет всем!
...
> Также есть наметки по верификации Джава с использованием Coq, но это
> планы совсем на будущее.
В эту сторону
http://krakatoa.lri.fr/
или без языка спецификаций?
>
> Если кто подобными вещами занимается (или кто знает, что кто-то
> занимается), напишите здесь плиз - интересно знать, насколько эта тема
> представлена в Питере.
>
Ну я так, интересуюсь, чтобы быть в курсе :)
Alexander Vlasov
> > планы совсем на будущее.
> В эту сторону
> http://krakatoa.lri.fr/
> или без языка спецификаций?
>
Немного в другую :). Я с кракатоа игрался некоторое время.
Но мне с ней трудно работать, ибо она не поддерживает Separation
Logic. Плюс
она основана на First Order логике.
А это значит, что составление спецификаций для heap - весьма
геморройное
дело.
Т.е. как исследовательский проект, это конечно круто, но на практике
это
очень трудоемко, вобщем я не асилил :).
В целом, я составил мнение, что системы основанные на First Order
Logic -
довольно муторны в плане спецификаций. А для меня - это основная
проблема.
Вобщем, я когда освоил Coq то понял, что Type Theory хоть и сложнее,
но все
же она дает больше возможностей в плане моделирования, а это более
важный
фактор.
Основная проблема у меня - это составление читабельных спецификаций,
с
доказательствами я как-нить разберусь, если сам пойму, что
написал :).
Поэтому, у меня появились некоторые наметки по верификации для Жабы,
которые
будут более практичны (по крайней мере для меня :)). Основная идея -
уйти от
JML, а писать спеки на основе Coq. Ну и плюс автоматизация а ля
invariant
detection, автоматическое преобразование циклов в рекурсию. Т.е.
переход из
пространства Джава, в пространство Coq. Не буду утвеждать, что JML
подход не
удачный, но лично у меня он не пошел.
Но это пока совсем на будущее, это куча работы, пока я себе более
реалистические задачи ставлю :).
> > Если кто подобными вещами занимается (или кто знает, что кто-то
> > занимается), напишите здесь плиз - интересно знать, насколько эта тема
> > представлена в Питере.
> Ну я так, интересуюсь, чтобы быть в курсе :)
Я тоже раньше интересовался, чтобы быть в курсе. А недавно решился
заняться :).
Yakov ZAYTSEV
я с этим сейчас разбираюсь. пишу компилятор, хочу писать некоторые модули на Coq
верификация Java.. верифицировали ведь JavaCard, где-то 300KLOC ушло..
Coq'а-то..
2009/11/9 Alexander Vlasov <glav...@gmail.com>:
>> > Также есть наметки по верификации Джава с использованием Coq, но это
>> > планы совсем на будущее.
>>
>> В эту сторону
>> http://krakatoa.lri.fr/
>> или без языка спецификаций?
>>
> Немного в другую :). Я с кракатоа игрался некоторое время.
> Но мне с ней трудно работать, ибо она не поддерживает Separation Logic. Плюс
> она основана на First Order логике.
> А это значит, что составление спецификаций для heap - весьма геморройное
> дело.
> Т.е. как исследовательский проект, это конечно круто, но на практике это
> очень трудоемко, вобщем я не асилил :).
> В целом, я составил мнение, что системы основанные на First Order Logic -
> довольно муторны в плане спецификаций. А для меня - это основная проблема.
> Вобщем, я когда освоил Coq то понял, что Type Theory хоть и сложнее, но все
> же она дает больше возможностей в плане моделирования, а это более важный
> фактор.
> Основная проблема у меня - это составление читабельных спецификаций, с
> доказательствами я как-нить разберусь, если сам пойму, что написал :).
> Поэтому, у меня появились некоторые наметки по верификации для Жабы, которые
> будут более практичны (по крайней мере для меня :)). Основная идея - уйти от
> JML, а писать спеки на основе Coq. Ну и плюс автоматизация а ля invariant
> detection, автоматическое преобразование циклов в рекурсию. Т.е. переход из
> пространства Джава, в пространство Coq. Не буду утвеждать, что JML подход не
> удачный, но лично у меня он не пошел.
> Но это пока совсем на будущее, это куча работы, пока я себе более
> реалистические задачи ставлю :).
>>
>> >
>> > Если кто подобными вещами занимается (или кто знает, что кто-то
>> > занимается), напишите здесь плиз - интересно знать, насколько эта тема
>> > представлена в Питере.
>> >
>>
>> Ну я так, интересуюсь, чтобы быть в курсе :)
>>
> Я тоже раньше интересовался, чтобы быть в курсе. А недавно решился заняться
> :).
> >
>
--
Best wishes,
Y
Alexander Vlasov
Да, я видел. Потому и подумал, что кто-то должен этим заниматься :).
> я с этим сейчас разбираюсь. пишу компилятор, хочу писать некоторые модули на Coq
>
А что за компилятор, если не секрет?
> верификация Java.. верифицировали ведь JavaCard, где-то 300KLOC ушло..
> Coq'а-то..
Пока на верификацию уходит много ресурсов, т.е. типа соотношение вроде
10 к 1 типично для большинства проектов, которые я видел
(доказательство требует на порядок больше ресурсов, нежели сама
программа). Именно, поэтому я не готов юзать верификацию в реальной
программерской работе, а иногда очень хочется (сложный рефакторинг, к
примеру).
Но это решаемо в перспективе :). По крайней мере, у меня основная
проблема - это специфицирование. Если есть "хорошая" спецификация, и
если расставить правильный промежуточные цели, то автоматические
пруверы все делают сами. Единственное, что чтобы эти хинты расставить,
нужно понимать что происходит, где прувер ступил :). Т.е. чтобы
промежуточные шаги доказательства были понятны человеку. По сути,
проблема в основном в выборе понятной человеку нотации и ясной
спецификации. Тогда можно жить, иначе мозги склеиваются :).
Yakov ZAYTSEV
про рефакторинг.
я не думал про это почти совсем, ну тут верификация пост-фактум (вы
ведь это имеете в виду) не нужна имхо
мне кажется: что здесь дело в том: что рефакторинг -- это работа
системы переписывания, так вот чтоб проверить, что "напереписывалось"
тож самое, что было в начале, значит проверить что нормальные формы
одинаковые, или просто, что две программы (терма) равны (стали, т.е.
оригинал и после рефакторинга)
т.е. мое мнение, что это из области Term Rewriting Systems.
так мои пять копеек
2009/11/9 Alexander Vlasov <glav...@gmail.com>:
--
Best wishes,
Y
Alexander Vlasov
В этой сфере все изначально сложно, но есть и некоторые подвижки :).
К примеру, у Микрософта есть весьма неплохой прувер Z3. Ну и у Coq
тактики тоже мощные.
У меня просто основная проблема - понять, что мне нужно и выразить это
в формальной форме.
Тогда я могу натравить автоматический прувер :).
Но вот понять и формализовать - это остается сложной задачей :).
>
> про рефакторинг.
> я не думал про это почти совсем, ну тут верификация пост-фактум (вы
> ведь это имеете в виду) не нужна имхо
> мне кажется: что здесь дело в том: что рефакторинг -- это работа
> системы переписывания, так вот чтоб проверить, что "напереписывалось"
> тож самое, что было в начале, значит проверить что нормальные формы
> одинаковые, или просто, что две программы (терма) равны (стали, т.е.
> оригинал и после рефакторинга)
> т.е. мое мнение, что это из области Term Rewriting Systems.
> так мои пять копеек
>
Вы правы, просто я имел в виду немного другое.
К примеру, у меня есть большая "лапша" на 3 экрана, и хочется ее
переписать, чтобы она работала быстрее/была понятнее. Простыми
реврайтами (которые есть в IDE к примеру) это делать не всегда реально/
практично.
Допусти я переписал метод с чистого лица. Соответственно, хотелось бы
иметь тулзу, которая бы автоматически проверила, что два варианта
одного метода эквивалентны, или выдавала бы список контрпримеров.
В принципе, в некоторых случаях эта задача решаемая (нет циклов/
рекурсии, либо они достаточно простые, к примеру, ограниченные сверху
небольшой константой). В общем же случае, надо написать спецификацию
для первого метода, проверить, что она соответствует реализации. Затем
написать другую реализацию и верифицировать ее относительно
спецификации. Тогда, соответственно, две реализации будут эквивалентны
(относительно спецификации).
Yakov ZAYTSEV
Alexander Vlasov
Ну тут проблемы нет, поскольку доказываются разные утверждения. Т.е.
нужно доказать две теоремы, что первая функция реализует спецификацию,
и что вторая реализация реализует эту же спецификацию. А вариантов
доказательств для каждой теоремы может быть сколько угодно.
Спецификация - это предикат, параметризованный функциями. На языке Coq
это будет так:
Coq < Section pi.
Coq < Require Import ProofIrrelevance.
Coq <
Coq < Variable spec : Set -> Prop.
spec is assumed
Coq < Variable func1 func2 : Set.
func1 is assumed
func2 is assumed
Coq <
Coq < Check proof_irrelevance (spec func1).
proof_irrelevance (spec func1)
: forall p1 p2 : spec func1, p1 = p2
Coq < Check proof_irrelevance (spec func1).
proof_irrelevance (spec func1)
: forall p1 p2 : spec func1, p1 = p2
Coq < End pi.
Yakov ZAYTSEV
это не нужно для рефакторинга имхо
к тому же как вы себе представляете-то? автоматическое создание
спецификаций из Java исходника и потом ее же проверка на новом
исходнике после тула?! :-)
серьезная тема имхо тянет на докторскую
2009/11/9 Alexander Vlasov <glav...@gmail.com>:
--
Best wishes,
Y
Alexander Vlasov
> это не нужно для рефакторинга имхо
> к тому же как вы себе представляете-то? автоматическое создание
> спецификаций из Java исходника и потом ее же проверка на новом
> исходнике после тула?! :-)
> серьезная тема имхо тянет на докторскую
Я зациклился, ибо это задача которая мне на практике встречалась,
которую я пока не решил :).
В качестве спецификации можно использовать и сам исходный код. Точнее
предполагается что спецификацией будет этот метод, при некоторых
ограничениях на входные параметры.
Выглядит это так: допустим у меня есть большая лапша без сайд эффектов
и циклов (либо с простыми циклами). Тогда я выделяю ее в отдельный
метод и пишу аналогичный метод, с теми же параметрами и результатом,
но другой реализацией. Ну и составляю теорему, типа что при таких-то и
таких-то ограничениях на входные параметры, результат двух методов
одинаков (эквивалентен, сопоставим по каким-то критериям).
При наличии циклов и рекурсии - это да докторская диссертация, не
менее :). Но более простые варианты тоже юзабельны, к примеру циклы
ограниченные небольшой константой сверху (т.е. unroll циклов дает
ацикличный CFG). А это уже реализуемо (я даже начал делать, но
заткнулся на проблеме циклов).
Maxim Taldykin
<glav...@gmail.com> написал:
...
> Допусти я переписал метод с чистого лица. Соответственно, хотелось бы
> иметь тулзу, которая бы автоматически проверила, что два варианта
> одного метода эквивалентны, или выдавала бы список контрпримеров.
