?

Log in

No account? Create an account
Contracts first - Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Contracts first [окт. 30, 2017|08:07 am]
Andy Melnikov
[Tags|, , , ]

Тут из альтернативной вселенной сообщают, что завтипы говно и не нужны.

Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers

Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
СсылкаОтветить

Comments:
[User Picture]From: maxim
2017-10-31 03:47 am

работают лучше



В репорте видно https://hal.inria.fr/hal-00766171/document
что пацаны писали для Эрго, а остальное для галоки (unusable)

Edited at 2017-10-31 03:48 (UTC)
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-10-31 04:02 am

Re: работают лучше

Дурак ты боцман, и шутки у тебя дурацкие - торпеды мимо прошли!

Какая нахуй индукция в FixedSizeBitVectors?
(Ответить) (Parent) (Thread)
[User Picture]From: maxim
2017-10-31 04:30 am

RE: Re: работают лучше

Мне похуй что ты пиздишь
1000M и слова "работают лучше" не вяжутся в одном предложении
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-10-31 06:59 pm

Re: работают лучше

А как ты можешь какие-то аргументы приводить, если ты не понял, что я сказал. При том в виде неподписанных табличек без ссылок на описание, что в этих табличках изображено. И, конечно, суть претензии я понял, просто это недостаточно хорошо сформулировано. Пример неудачный, лимиты потребления ресурсов смешные и т.п. Надо, чтобы у нас была такая бумажка, чтобы ни Швондер, ни кто либо другой не мог даже подойти :)

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

Там же море говнотехнологий. Я щитаю, надо иметь домашние заготовки для ответа на вопросы в духе "а зачем это всё, когда есть Х".
(Ответить) (Parent) (Thread)
[User Picture]From: maxim
2017-10-31 10:16 pm

RE: Re: работают лучше

> Считай это провокационным предложением написать популярный пост
Я знаю как отвечать на эти вопросы и для них есть место в дисере, а не в ЖЖ перед первым попавшимся мудаком.
(Ответить) (Parent) (Thread)
[User Picture]From: mnogo_hodovka
2017-10-31 07:39 pm

Re: работают лучше

Вот, кстати, непонятно, чем продукт от Groupoid Infinity будет лучше, чем SPARK. 99,9% кода в самолетах Boeing и не знаю сколько (но много) кода в самолетах Airbus написаны инженерами на Ada SPARK. Все верифицировано безо всяких зависимых типов, авионика стабильна, самолеты летают. Индустрия консервативна, она уже приняла SPARK и использует его в авиации, железных дорогах, атомных реакторах, медицинском оборудовании. Если интересно, посмотрите, как там все это делается:

http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_example/basic.html

В общем случае там применяется гибридная верификация:

https://bldl.ii.uib.no/2014/14v-bldl-TuckerTaft-sparc_proof_test.pdf

https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/03-ada-spark.pdf

Некоторые вещи проверяются тестами, некоторые - прувами. Но там можно вообще отказаться от юнит-тестов и для всего всегда использовать formal proofs.
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-11-06 07:21 pm

Re: работают лучше

Там этих технологий целый зоопарк, т.е. не только верификация а ля спарк и завтипы. ACL2 вот например тоже широко применяется

http://www.cs.utexas.edu/~marijn/publications/ACL2-ARCADE.pdf

Различных направлений верификации очень много. Вот например подход, отличающийся от всех остальных (завтипов, нетипизированных доказательств ACL2/Vampire, верификации в cтиле https://en.wikipedia.org/wiki/Extended_static_checking используемой в SPARK/Why3)

https://sv-comp.sosy-lab.org/2018/benchmarks.php

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

Все эти технологии имеют достаточно ограниченное применение. Так,
SPARK неприменим за пределами тайт-лупов без использования кучи, используемых в хард-реалтайм системах. Собственно направление зависимых типов (Сoq, Agda, Idris, HOL) в этом плане не отличается от любых других.

Так что не надо тут пиздеть. Пишите конструктивно!
(Ответить) (Parent) (Thread)
[User Picture]From: gabriel_irk
2017-11-09 12:07 pm

Re: работают лучше

Строго говоря, в HOL нет зависимых типов. :) Но суть, безусловно, та же самая.
(Ответить) (Parent) (Thread)
[User Picture]From: gabriel_irk
2017-10-31 08:54 am
В этой альтернативной реальности и для Eiffel статический прувер есть: http://se.inf.ethz.ch/research/autoproof/

Я с ним немного работал и только укрепился во мнении, что зав. типы гораздо лучше.
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-10-31 07:06 pm
Ну если вы немного поработали с чем угодно, вы будете плеваться. Разработчики Singularity (там внутри прототип Boogie, внутри которого Z3) говорили (в качестве недостатка технологии), что надо знать, как устроен Z3, чтобы не давать ему "неправильные" инварианты, которые он доказать не сможет.
(Ответить) (Parent) (Thread)
[User Picture]From: gabriel_irk
2017-11-09 12:06 pm
Лично у меня наоборот - я обычно в восторге от инструментов, с которыми работал немного, а плююсь на то с чем прилично поработал и пособирал граблей. :)

У Autoproof (да и Eiffel в целом), к сожалению, грабли начинаются почти сразу и в большом количестве.

С контрактами и их верификацией на Z3 (особенно через посредников как Boogie) есть несколько проблем.

Контракты обычно пишутся на том же языке, что и код, который обычно Тьюринг-полный, что препятствует верификации само по себе. Если же ограничить язык контрактов, то придётся учить 2 языка, а в зав. типах всё на одном пишется.

Но более существенная проблема - семантическое расстояние между языком контрактов и программ и ассертами Z3 (SMTLIB в целом). Одна из граней проблемы - те самые "неправильные" инварианты и вообще всяческие подсказки для Z3 чтобы он лучше и быстрее работал. Тащить это в язык контрактов как-то диковато. Другая сторона - возникновение промежуточного семантического слоя в виде явного языка (Boogie) или неявного. В частности, Boogie по факту оказывается чистым функциональным языком, поскольку явно "протаскивает" кучу через аргументы и явно отслеживает все (потенциальные) изменения в ней. И другого способа формализовать императивное программирование в общем-то нет.

И программисту всё равно приходится изучить и понять это внутреннее представление, потому что даже правильные теоремы не всегда автоматически доказываются - приходится разбираться почему доказательство "заткнулось" и дописывать леммы или переформулировать теорему "попонятнее".

Поэтому у меня возникает вопрос: почему бы сразу не писать на функциональном языке с зав. типами чтобы за доказательствами далеко не ходить? В том же F* (или Liquid Haskell) трансляция в SMTLIB достаточно прямолинейна и вполне поддаётся отладке.

Ну и ещё есть соображения практического удобства...
(Ответить) (Parent) (Thread)