Здравствуйте, gandjustas, Вы писали:

[snip]

G>Можно, если у тебя есть спецификация. А если нет, то вообще непонятно зачем ты код написал.

Да не писал я никакого кода.

SH>>>>>Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п.
D>>>>Даже для
D>>>>

D>>>>sum x y = x + y
D>>>>

D>>>>?

А>>>А если в спецификации было написано "реализовать функцию вычитания целых чисел с именем sub"?
D>>Не уловил подвох.

А>Подвох в том, что глядя даже на такую простую штуку как
А>

А>sum x y = x + y
А>

А>нельзя сказать есть в коде бага или нет.

Выше история сообщений. В исходном примере (который написал не я) ни о какой спецификации речи нет. Там только вопрос можно-ли доказать отсутсвие багов для такого кода. Как я понял, имелось в виду, что уж в таком простом случае никакой ошибки не может быть в принципе. На это я ответил, что если в спецификации было написано, что нужно реализовать вычитание, то код ошибочный. Собственно, о том и речь, что о правильности кода можно говорить только когда есть и код и спецификация.

Здравствуйте, thesz, Вы писали:

T>>>>>Для зависимых типов не нужен запуск программы. Для контрактов нужен.
G>>>>Неправда.
T>>>http://rsdn.ru/forum/philosophy/3395836.1.aspx

Автор: thesz
Дата: 19.05.09

T>>>Проверь контрактом во время компиляции факт правильного упорядочения списка.
G>>Его контрактом даже описать не получится.
T>Ну, а в зависимых типах это возможно.
В .NET кстати есть IOrderedEnumerable, IOrderedQueryable которые как раз обозначают упорядоченную последовательность.
После того поста я начал активно их использовать.

G>>А то что получается описывать контрактом проверяется статически.

T>Перечисли, пожалуйста, что же можно проверить контектом.
Много чего, только не получится расширить существующие типы для обеспечения проверок. Поэтому упорядоченность списка не получится прверить.

Здравствуйте, thesz, Вы писали:

T>>>Список с доказательством имеет структуру, аналогичную обычному списку. Все доказательства изъяты на момент компиляции.
T>>>Поэтому, несмотря на "необходимость преобразований", расходы будут нулевыми.
G>>Это я понимаю.
G>>А в коде как оно выглядеть будет?
G>>Есть например две функции
G>>

G>>sort : List Nat -> OList 0
G>>otherFunc : List Nat -> не_важно_что
G>>

G>>Можно ли записать композицию sort >> otherFunc (или как оно там пишется) или нужны еще какие-то телодвижения?

T>Нужны телодвижения.
И как они будут выглядеть?

Здравствуйте, thesz, Вы писали:

VD>>К тому же я практически уверен, что юнит-тесты от этого не исчезнут. Юнит-тесты проверяют поведение, а описать поведение статически просто невозможно. Это и есть код.

T>Боже ж мой.
T>Код и есть статическое описание поведения.
T>То есть, мы статически — кодом, ведь код-то не меняется во время исполнения, — описываем поведение программы.
T>Таким образом, поведение описывается исключительно статическим образом. Даже если это тесты.

Ты видимо не понял. Если можно написать спецификацию поведения некоторого объекта, то эта спецификация будет не проще самого кода объекта, вероятнее всего гораздо сложнее. Как потом доказать что спецификация написана без ошибок?

Здравствуйте, dotneter, Вы писали:

D>Я надеялся что мы еще в контексте предыдущего примера.

Да не вопрос. Я просто воспользовался удачно подвернувшимся случаем

D>Это баг спецификации а не реализации.

А в чём разница?
Особенно, если мы умеем спецификацию формально преобразовывать в реализацию?

Реализация более верхнего уровня это спецификация для более нижнего. Реализация на С это спецификация для компилятора. Машинный код, генерируемый компилятором это спецификация для процессора. Микрокод инструкции это спецификация для кусочков процессора... Ниже, пожалуй некуда, ниже сильно всё меняется, да и про микрокод я уже не уверен.

Но тем не менее, ошибка в любом из уровней это баг. Только в одном случае это проектировщики проектировали, проектировали, да не выпроектировали, во втором -- програмисты программировали да не выпрогрммировали, в третьем -- компиляторы не выкомпилировали и т.п. Даже если мы всё доказали кроме первого уровня, что безусловно огромное достижение, сказать, что в программе "багов нет и это доказано" нельзя.

Можно доказать соответствие модели. Нарисовать конечный автомат какой-нибудь Доказать, что в нём нет каких-нибудь плохих путей. Или что все пути обладают каким-то свойством и т.п. Но _доказать_ соответствие модели задаче невозможно. Математика, как и возможность доказательства, _начинается_ с модели. На предшествующем этапе нет ни математики ни доказательства. Модель можно только опровергнуть. В положительную строну -- можно поставить много экспериментов и убедиться, что результаты правильные. Но ведь это не доказательство.

Здравствуйте, SergH, Вы писали:

SH>А в чём разница?
В глобальном смысле наверное не в чем. В практическом же, нужно принять уровни которые считаются по определению правильными и на основе чего можно делать выводы о правильности реализации.
sum x y = x + y
Предполагается правильность спецификации и +. Да если одно из этим предположений не верное, то и все решение ошибочно, но я не вижу смысла в данном подходе.

Здравствуйте, WolfHound, Вы писали:

WH>Только при наличии аннотаций которые более многословны чем зависимые типы и покрывают куда меньше утверждений.

Многословность != непонятность. Сравним два варианта:

zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

и

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
  requires l1.Lenght == l2.Lenght
  ensures  value.Lenght == l1.Lenght

WH>А никто не обольщается. Но отказываться от проверок на этапе компиляции это просто глупо.

Не спорю. Но проверки не должны вносить неоправданную сложность. Они должны быть понятным простым смертным.

WH>И вообще эта твоя реплика очень сильно смахивает на отмазки любителей динамической типизации... типа "У нас и так все работает! Нахрена нам статические проверки!?"

Мало ли что на что смахивает? Меня вряд ли можно заподозрить в любви к динамике. Но и любить чистую науку мне как-то тоже не охота. Меня интересует практика. А практика — это всегда компромисс.

VD>>Основной причиной появления багов является сложность задачи. И если система которая должна уберечь от багов будет увеличивать эту самую сложность, то на практике будет ровно противоположенный ожидаемому результат.
WH>А она увеличивает?

Приведенный тобой пример описания типа функции в двое длиннее тела функции и в 10 раз не понятнее (на мой взгляд).

WH>А если вспомнить про то что такая система типов еще и кучу тестов делает бессмысленными?

Кучу ли? Что у нас с динамическими списками? Что у нас с вводом / выводом?
Что, наконец с логикой? Как в систему типов загнать информацию о поведении не тривиального кода?

VD>>Ну, а то что мы тут увидели вряд ли можно назвать простым.
VD>>В прочем, возможно я "не догоняю".
WH>Я таки думаю что не догоняешь.
WH>Ибо зависимые типы по началу выносят мозг покруче чем функциональщина императивщику...

Я не заметил чего-то выносящего мозг. Видимо по второму разу данная трава уже не так выносит .
Я заметил "много букв" при не вполне понятном результате.

В общем, здесь

Автор: VladD2
Дата: 03.07.09

я задал несколько вопросов. Ответь на них. Может это прояснит кое-что.

Я не догматик и умею менять свое мнение. Пока что оно умеренно скептическое. В прочем, скепсис скорее относится к синтаксису и возможностям, а не к самой идее.

Здравствуйте, dotneter, Вы писали:

D>sum x y = x + y
D>Предполагается правильность спецификации и +.

+ это нижний уровень относительно sum. Я говорю про верхний.

Здравствуйте, deniok, Вы писали:

D>Мечта — это чтобы программы сами писались?
D>Зависимые типы позволяют довольно удобно записывать широкий класс спецификаций. Например, отсортированный список на Агде можно описать так:
D>

D>data OList : Nat -> Set where 
D>  Nil  : {b : Nat} -> OList b 
D>  Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
D>

Сначала хочется пояснить для тех кто в курсе этой агрды, что для непосвященных это не более чем кракозябры. Все эти Nat-ы и Set-ы просто не определенные понятия. Так что хотите кому-то что-то объяснить, разжёвывайте по мельче.

D>Теперь функция с типом
D>

D>sort : List Nat -> OList 0
D>

D>либо не компилируется, либо гарантированно возвращает отсортированное.

Замечательно. И как будет выглядеть описание скажем функции получающей на входе текстовый файл, и выдающей на выходе АСТ распознанного языка и/или список ошибок? И что это описание может доказать?
Другими словами, какова практическая ценность данного подхода?

А то примитивы вроде функции сортировки и так проверяются на раз. А пишутся они очень редко.

Сложность же начинается там где есть огромные объемы входных данных, большое количество параметров чье сочетание дает очень разнообразный результат, а некоторые из сочетаний не имеют смысла. В таких условиях многие граничные ситуации просто игнорируются программистом и не получают должного уровня обработки, что в некоторых случаях вылезает в виде багов во время исполнения.
Так вот проблем не в том, что эти случаи сложно обработать, а в том, что код их обработки во много раз увеличивает общий код приложения. И если ссистема типов начнет заставлять меня обрабатывать все подобные случаи, то я заплачу и убегу .

Здравствуйте, dotneter, Вы писали:

SH>>Для доказательства нужно формально сравнить "что хотелось" и "что получилось". Проблема в том, что "что хотелось" в формальном виде отсутствует.
D>sum x:int y:int — хочется Х (Х — спецификация оператора +)
D>получилась реализация
D>sum x:int y:int = x + y
D>которая эквивалентна операции + которая по определению является правильной, следовательно sum удовлетворяет тому что хотелось и является правильной.

Это называется определение через себя. Стандартная логическая ошибка. Самоопределение конечно всегда верно, но при этом совершенно бессмысленно.

Здравствуйте, dotneter, Вы писали:

D>Это баг спецификации а не реализации.

А вот это уже никого кроме философов не трогает. Баг — это работа программы не так как предполагает ее пользователь.
Если тривиальщину выразить трудно, то что делать со сложным софтом?

Здравствуйте, SergH, Вы писали:

SH>Реализация более верхнего уровня это спецификация для более нижнего. Реализация на С это спецификация для компилятора. Машинный код, генерируемый компилятором это спецификация для процессора. Микрокод инструкции это спецификация для кусочков процессора... Ниже, пожалуй некуда, ниже сильно всё меняется, да и про микрокод я уже не уверен.

Не. Спецификация не подразумевает полное описание системы. Спецификация всегда подразумевает умолчания и упрощения. Маш.код и ассемблер — это просто разные представления одного и того же. С-и и ассемблер тоже. Но С ближе к людям. В прочем в С уже есть некоторые умолчания, но они формализованы стандартом языка.

Именно по этому спецификации пишутся на неформальных языках и претворяются в жизнь программистами. Иначе мы имеем некий ДСЛ для которого нужно всего лишь написать транслятор. В таком случае доказать нужно уже не корректность программы, а корректность кодогенератора и ДСЛ-я.

G>>>Можно ли записать композицию sort >> otherFunc (или как оно там пишется) или нужны еще какие-то телодвижения?

T>>Нужны телодвижения.
G>И как они будут выглядеть?

Мы можем автоматически получить преобразование из спископодобной структуры в список. Это сделает компилятор. См. Generic programming with dependent types.

Использование любой спископодобной (даже чисел Пеано!) структуры как параметра-списка сведётся к вызову этого автоматического преобразования.

Иными словами: onSortedList soertList = ... (onSimpleList (toList soertedList)) ...

Здравствуйте, gandjustas, Вы писали:

G>Ты видимо не понял. Если можно написать спецификацию поведения некоторого объекта, то эта спецификация будет не проще самого кода объекта, вероятнее всего гораздо сложнее. Как потом доказать что спецификация написана без ошибок?
Это чисто интуитивная мысль, или есть какие-то подтверждения?
Спецификация отсортированного списка, как было видно на примере, на порядки проще сортировки. Так что "вероятнее всего" стоит здесь вероятнее всего не к месту.

Здравствуйте, gandjustas, Вы писали:

G>Здравствуйте, thesz, Вы писали:

VD>>>К тому же я практически уверен, что юнит-тесты от этого не исчезнут. Юнит-тесты проверяют поведение, а описать поведение статически просто невозможно. Это и есть код.

T>>Боже ж мой.
T>>Код и есть статическое описание поведения.
T>>То есть, мы статически — кодом, ведь код-то не меняется во время исполнения, — описываем поведение программы.
T>>Таким образом, поведение описывается исключительно статическим образом. Даже если это тесты.

G>Ты видимо не понял. Если можно написать спецификацию поведения некоторого объекта, то эта спецификация будет не проще самого кода объекта, вероятнее всего гораздо сложнее.

"Вероятней всего" — это откуда такая оценка? Есть исследования?

G>Как потом доказать что спецификация написана без ошибок?

Есть такая штука, называется тройки Хоара. Выглядят так:
{Q} S {P}

Лет этой штуке не счесть.

С её помощью были разработаны многие алгоритмы, часто весьма и весьма нетривиальные.

Есть такая книга, Program Construction: calculating implementation from specification, которая рассказывает про то, как применять тройки Хоара к реальным задачам.

По чтению этой книги у меня сложилось впечатление, что большая часть реализации вытекает из внешней спецификации и спецификаций на доступные компоненты. Вытекает сама собой, просто при рассуждении оказывается так, что в большинстве мест могут быть подставлены только вполне определённые компоненты. Другие просто не подходят.

Моментов ключевого выбора раз, два и обчёлся.

Если ты посмотришь на свои программы и на то, как ты их создаёшь, то ты обнаружишь ровно то же самое.

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

Здравствуйте, VoidEx, Вы писали:

VE>Здравствуйте, gandjustas, Вы писали:

G>>Ты видимо не понял. Если можно написать спецификацию поведения некоторого объекта, то эта спецификация будет не проще самого кода объекта, вероятнее всего гораздо сложнее. Как потом доказать что спецификация написана без ошибок?
VE>Это чисто интуитивная мысль, или есть какие-то подтверждения?
Интуитивная.

VE>Спецификация отсортированного списка, как было видно на примере, на порядки проще сортировки. Так что "вероятнее всего" стоит здесь вероятнее всего не к месту.
Спецификация списка != спецификация алгоритма сортировки.

В любом случае полная (а иначе она нам не поможет) спецификация поведения кода будет не меньше (и не проще) самого кода.

Здравствуйте, thesz, Вы писали:

VD>>К тому же я практически уверен, что юнит-тесты от этого не исчезнут. Юнит-тесты проверяют поведение, а описать поведение статически просто невозможно. Это и есть код.

T>Боже ж мой.
T>Код и есть статическое описание поведения.
T>То есть, мы статически — кодом, ведь код-то не меняется во время исполнения, — описываем поведение программы.
T>Таким образом, поведение описывается исключительно статическим образом. Даже если это тесты.

Если исходить из этого, то прав SergH

Автор: SergH
Дата: 03.07.09

, в том смысле, что багов не бывает.

T>Я бы понял, если бы ты сослался на проблему останова, но ты же про неё не знаешь, ведь так?

Знаком. Только я не о том. Я о том, что спецификации большинства программ не формальны. Их не выразить в системе типов. Точнее задача выражения может оказаться сложнее задачи реализации. А формальные спецификации можно (как верно заметил SergH) превратить в корректные программы написав годогенератор. Это будет во много раз проще.

Юнет-тесты тем и хороши, что проверяют важные для пользователей факты. В прочем, случалось видеть и совершенно бессмысленные юнит-тесты проверяющие правильность работы ALU. Но это уже проблемы тугодумов.

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

Здравствуйте, gandjustas, Вы писали:

G>Спецификация списка != спецификация алгоритма сортировки.
Это просто придирка или ты намекал, что List a -> SortedList a сложнее самой сортировки?

Здравствуйте, WolfHound, Вы писали:

WH>Эту кракозябру можно написать немного короче:
WH>

WH>zip : forall{A B n} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
WH>

Кстати, так уже намного лучше. Это гипотетический синтаксис или Агда?

Не ясно только зачем нужен "forall{A B n} -> ". Это объявление явно лишнее и сбивает с толку.

T>>Таким образом, поведение описывается исключительно статическим образом. Даже если это тесты.

VD>Если исходить из этого, то прав SergH

Автор: SergH
Дата: 03.07.09

, в том смысле, что багов не бывает.

T>>Я бы понял, если бы ты сослался на проблему останова, но ты же про неё не знаешь, ведь так?

VD>Знаком. Только я не о том. Я о том, что спецификации большинства программ не формальны. Их не выразить в системе типов.
VD>Точнее задача выражения может оказаться сложнее задачи реализации.

Может? А может не оказаться? А каково соотношение этих двух случаев?