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

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>>>

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

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

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

G>>А можно ли потом такой передать как обычный список в другую функцию? Будет неявное реобразование типа? Потребуется ли явное преобразование или может еще какие операции?

T>Список с доказательством имеет структуру, аналогичную обычному списку. Все доказательства изъяты на момент компиляции.

T>Поэтому, несмотря на "необходимость преобразований", расходы будут нулевыми.

Это я понимаю.

А в коде как оно выглядеть будет?
Есть например две функции

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

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

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


SH>Тогда, я считаю, багов не существует в природе. Можешь привести пример бага?

sum x y = x - y

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

G>Его контрактом даже описать не получится.

Инварианты класса?

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

SH>>Тогда, я считаю, багов не существует в природе. Можешь привести пример бага?
D>

D>sum x y = x - y
D>

Это не баг. Это была нужна функция x — y. Потребуется другая -- будет написана sum2.

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

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

вот об этом процессе и идёт речь. в C# или хаскеле он не поддерживается

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

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

G>>Его контрактом даже описать не получится.

D>Инварианты класса?

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

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

SH>Это не баг. Это была нужна функция x — y. Потребуется другая -- будет написана sum2.

sum x:int y:int — хочется Х (Х — спецификация оператора +)
получилась реализация
sum x:int y:int = x — y
Это баг

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

D>Здравствуйте, Аноним, Вы писали:

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

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

sum x y = x + y

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

Здравствуйте, Аноним, Вы писали:

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

D>>Здравствуйте, Аноним, Вы писали:

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

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

А>sum x y = x + y
А>

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

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

Здравствуйте, Аноним, Вы писали:

А>Это если считать обычным подходом код без модульных тестов и без проверок параметров функции. Если первое неплохо автоматизируется с помощью того же PEX (сам пока не пользовался, но допустим), то от второго, вроде как, никуда не денешься. Хотя, на первый взгляд, да, действительно громоздко.

Вот именно. Очень громоздко и на тот самый первый взгляд (как минимум) невнятно.

А>Во всяком случае, без дополнительного изучения, так однозначно отвергать эту штуку не стоит,

Дык я давно вырос из возраста когда отвергают все и вся с пеной изо рта, и пока не дожил до возраста когда скептически скрипят на все подряд.

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

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

А>или за твоими словами кроется некий опыт использования/изучения этого подхода? В таком случае, было бы очень интересно услышать подробности.

С данным подходом я не сталкивался. Я возился с системами доказательства корректности ПО. Это не тоже самое, но преследует схожие цели.

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

VD>>Статическая верификация кода возможна и так.
D>Имхо, основной вопрос в том насколько сложно реализовывать верификаторы, и насколько сложные задачи они могут решать.
D>Конечно если у нас есть мега интеллектуальная система которая выявляет любые ошибки, то нам не только не нужна мощная система типов, нам и сами типы нужны.

Согласен. Основная проблема верификторов в том, что для них требуется дополнительная разметка кода. Скажем чтобы верификатор контролировал недопустимость null-ов в параметрах нам нужно пометить параметры особым образом. А если такая пометка не обязательна, то программист (даже не очень ленивый) с большой вероятностью забьет на это. Причем с null проблема решается введением по умолчанию недопустимости null. А вот с инвариантами и т.п. значительно хуже.

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

SH>>Это не баг. Это была нужна функция x — y. Потребуется другая -- будет написана sum2.

D>sum x:int y:int — хочется Х (Х — спецификация оператора +)
D>получилась реализация
D>sum x:int y:int = x — y
D>Это баг

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

Теперь ты говоришь, что подразумевал вот такой вот эталон. Ладно.

Но ведь программист в здравом уме и трезвой памяти написал код x — y. Компьютер понял его буквально и так и выполнил. Потом программист спохватился и понял, что надо x+y.

Чем это отличается от того, что ты, в здравом уме и трезвой памяти напишешь

sum x:int y:int — хочется Х (Х — спецификация оператора +)

И формально докажешь даже. Или формально преобразуешь в код.

А потом спохватишься и поймёшь, что нужно

sum x:int y:int — хочется Х (Х — спецификация оператора -)

Это баг или не баг? Если нет, то почему? Чем одно от другого отличается?
Если да -- то ведь доказали же только что. Значит не совсем то доказали.

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

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

T>>Проверь контрактом во время компиляции факт правильного упорядочения списка.
G>Его контрактом даже описать не получится.

Ну, а в зависимых типах это возможно.

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

Перечисли, пожалуйста, что же можно проверить контектом.

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

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

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

Нужны телодвижения.

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

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


SH>>Тогда, я считаю, багов не существует в природе. Можешь привести пример бага?
D>

D>sum x y = x - y
D>

Метрика Минковского — d^2=c^2*t^2-r^2 — это ошибочная запись обычной метрики пространства (d^2=c^2*t^2+r^2).

Зато какие интересные эффекты мы видим из-за этого!..

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

I've come up with a set of rules that describe our reactions to technologies:
1. Anything that is in the world when you're born is normal and ordinary and is just a natural part of the way the world works.
2. Anything that's invented between when you're fifteen and thirty-five is new and exciting and revolutionary and you can probably get a career in it.
3. Anything invented after you're thirty-five is against the natural order of things.
— Douglas Adams

Сколько тебе лет?

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

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


SH>Это баг или не баг? Если нет, то почему? Чем одно от другого отличается?
SH>Если да -- то ведь доказали же только что. Значит не совсем то доказали.

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

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

Боже ж мой.

Код и есть статическое описание поведения.

То есть, мы статически — кодом, ведь код-то не меняется во время исполнения, — описываем поведение программы.

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

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

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

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

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

WH>теперь напишем тело этой кракозябры
WH>

WH>zip []    []    = []
WH>zip x::xs y::ys = (x, y) :: zip xs ys
WH>

WH>Все. По другому хрен напишешь ибо компилятор надает по рукам.

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

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

ОК. А что мы контролировали? И нельзя ли выразить это более просто?

WH>Теперь как это будет выглядеть на немерле
WH>

WH>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
WH>

WH>Различия только в том что в случае с зависимыми типами указана длинна списков.

Я бы так не сказал. В немероловм варианте есть простор для фантазии (так как реализация не приведена).

Списки могут различаться по длине и при этом реализация может реагировать по разному:
1. Выдать исключение.
2. Отбросить "лишние" элементы из более длинного списка.

По жизни второй вариант будет более востребован, хотя потребоваться могут оба.

Код который нужно добавить, чтобы получить п. 1. не сложен:

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

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

Как эти проблемы решаются в Агде?

WH>

WH>{
WH>| ([],    [])    => []
WH>| (x::xs, y::ys) => (x, y) :: zip(xs, ys)
WH>| _              => throw InvalidArgumentException()
WH>}
WH>

WH>те в результате мы и написали больше и переложили проверку с компилятора на рантайм.

Я повторюсь, но мне не понятно, как компилятор сможет проверить работу со списками большая часть которых получается динамически?

Или мы будем работать отдельно с динамическими списками (и при этом все проверки пойдут на смарку), и отдельно со статическими?

WH>И после этого ты говоришь что зависимые типы сложнее?

Я пока ничего не говорю. Я просто констатирую факт, что то что ты привел — это весьма туманно, сложно и при этом не понятно решает ли исходные задачи.

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

BZ>ты можешь *доказать*, что некая программа не содержит багов?

Я могу доказать обратное.

А вообще — это и не надо на практике (если конечно речь не идет о жизи людй и т.п.). Основная задача — сделать процесс разработки проще. Недопущение багов или их статическое выявление — это средство решения данной задачи. Но если средство усложняет жизнь еще больше чем проблема которую оно решает, то это вредительство, а не помощь.

Что мне толку со знания о корректности кода если на его написание я потратил в 10 раз больше чем я потратил бы на его написание и отладку традиционными средствами?