Здравствуйте, BulatZiganshin, Вы писали:
BZ>ты можешь *доказать*, что некая программа не содержит багов?
Это зависит от того, что такое "баг".
Программа она же дура. Она делает, что ей скажут. Что написано, то и сделала -- с этой точки зрения багов не просто нет, их практически не существует, кроме сбоев аппаратуры.
Баг это отличие программы от спецификации. Или отличие спецификации от "того, что имелось ввиду". Имея на руках только программу ни то ни другое доказать невозможно. Если есть формальная спецификация, по которой можно что-то доказывать, то скорее всего её можно формально и преобразовать в программу, т.е. "формальная спецификация" это программа и есть. Осталась только разница между спецификацией и мечтой, и вот она видимо неустранима и соответствие не доказать.
Но иногда можно доказать какие-нибудь параметры, типа того, что никогда не виснет, или что задержка при ответе не больше чем, и т.п. Но это не "отсутствие багов".
Здравствуйте, BulatZiganshin, Вы писали:
BZ>ты можешь *доказать*, что некая программа не содержит багов?
Доказать можно только формальные утверждения.
Утверждение "программа не содержит багов" не формализуемо. Те доказано быть не может.
Но мы можем доказать соответствие спецификации, а это уже очень и очень не мало.
В любом случае зависимые типы убивают кучу тестов. Остаются только функциональные на случай если в спецификации написано не то что должно быть там написано.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, VladD2, Вы писали:
VD>Статическая верификация кода возможна и так. Вон в 4-ом фрэйворке вроде как будет поддерживаться для реальных систем.
Только при наличии аннотаций которые более многословны чем зависимые типы и покрывают куда меньше утверждений.
VD>Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки. Баги сазажают люди. Если алгоритм крив, то никакая верификция или мощная система типов не спасет. Не надо обольщаться.
А никто не обольщается. Но отказываться от проверок на этапе компиляции это просто глупо.
И вообще эта твоя реплика очень сильно смахивает на отмазки любителей динамической типизации... типа "У нас и так все работает! Нахрена нам статические проверки!?"
VD>Основной причиной появления багов является сложность задачи. И если система которая должна уберечь от багов будет увеличивать эту самую сложность, то на практике будет ровно противоположенный ожидаемому результат.
А она увеличивает?
А если вспомнить про то что такая система типов еще и кучу тестов делает бессмысленными?
VD>Ну, а то что мы тут увидели вряд ли можно назвать простым. VD>В прочем, возможно я "не догоняю".
Я таки думаю что не догоняешь.
Ибо зависимые типы по началу выносят мозг покруче чем функциональщина императивщику...
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, SergH, Вы писали:
SH>Баг это отличие программы от спецификации. Или отличие спецификации от "того, что имелось ввиду". Имея на руках только программу ни то ни другое доказать невозможно. Если есть формальная спецификация, по которой можно что-то доказывать, то скорее всего её можно формально и преобразовать в программу, т.е. "формальная спецификация" это программа и есть. Осталась только разница между спецификацией и мечтой, и вот она видимо неустранима и соответствие не доказать.
Мечта — это чтобы программы сами писались?
Зависимые типы позволяют довольно удобно записывать широкий класс спецификаций. Например, отсортированный список на Агде можно описать так:
data OList : Nat -> Set where
Nil : {b : Nat} -> OList b
Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
Теперь функция с типом
sort : List Nat -> OList 0
либо не компилируется, либо гарантированно возвращает отсортированное.
Здравствуйте, deniok, Вы писали:
D>Мечта — это чтобы программы сами писались?
Мечта это "то, что имелось ввиду".
D>Зависимые типы позволяют довольно удобно записывать широкий класс спецификаций. ...
Не, не, я понимаю, что это ещё один ещё более высокоуровневый язык и это наверное хорошо, если в этом разобраться.
Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п.
Здравствуйте, SergH, Вы писали:
SH>Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п.
Даже для
Здравствуйте, dotneter, Вы писали:
SH>>Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п. D>Даже для http://rsdn.ru/forum/decl/3454285.1.aspx
Давайте выделим ветку? И в философию её... Оффтоп идёт.
D>Даже для D>
D>sum x y = x + y
D>
D>?
Для доказательства нужно формально сравнить "что хотелось" и "что получилось". Проблема в том, что "что хотелось" в формальном виде отсутствует.
Если нужен пример, когда стандартное компьютерное сложение работает неинтуитивно -- возьми число с плавающей точкой побольше, и прибавь к нему 1. Не знаю, как в Хаскеле, в Питоне используются стандартные double из С, со всеми вытекающими. Плавающего числа около 10^17 должно быть достаточно...
Подразумевал ли автор, что ему нужно складывать такие числа? А кто его знает. Формальных критериев нет. С другой стороны, это ограничение не функции, а типа данных. А как должна вести себя функция, нарвавшись на такое ограничение? Опять непонятно. Может она правильно себя ведёт, а может подразумевалось что-то другое.
А я собственно намекаю, что "что хотелось" это принципиально неформализуемое понятие. Потому что когда оно формализовано это уже другая сущность -- спецификация. В процессе формализации что-то может потеряться, и формальным способом это потерявшееся не найти.
Здравствуйте, Аноним, Вы писали:
А>Здравствуйте, BulatZiganshin, Вы писали:
BZ>>Здравствуйте, VladD2, Вы писали:
VD>>>Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки. Баги сазажают люди. Если алгоритм крив, то никакая верификция или мощная система типов не спасет. Не надо обольщаться.
BZ>>ты можешь *доказать*, что некая программа не содержит багов?
А>В общем случае этого никто не может. Кстати, доказательства (особенно достаточно сложные) также могут содержать ошибки, так что даже наличие доказательства безошибочности программы отнюдь не гарантирует отсутсвие ошибок в этой программе.
В данном случае доказывает компьютер, а он не ошибается.
А>Кроме того интересует насколько дорого обходится повышение качества программы посредством использования доказательств. Скажем, рассмотрим такой пример (все цифры взяты с потолка). Мы создаём некоторое ПО (не для управления ядерным реактором). Используя привычные средства повышения качества (модульные тесты, ревью кода) имеем 10 ошибок на 1000 строк кода (взято с потолка) и затрачиваем на это X ресурсов. Если мы воспользуемся зависимыми типами докажем, что у нас 0 ошибок на 1000 строк кода, но потратим на это 2X ресурсов, то зачем нам это доказательство?. ИМХО, гораздо интереснее узнать, как именно влияют зависимые типы на качество и стоимость ПО, нежели абстрактная возможность "доказать" отсутвие ошибок для некоторых программ.
Ты рассматриваеш ситуацию полярно — либо "стандартные" средства, либо статические проверки.
На самом деле несть континуум промежуточных "состояний".
Сначала ты пользуешься элементарными типами для проверки правильности кода — возвращает ли метод строку или число (катсти в динамических языках даже такие мелочи надо тестировать), потом используешь более сложные конструкции, которые тебе позволяют ограничить множества входных и выходных значений для элементарных типов. Далее, если позволяет язык, уже используются типы, которые описывают некоторые свойства сложных объектов, на каждом этапе сложность описываемых объектов возрастает.
Компилятор естественно статически проверяет, что в процессе работы программы эти свойства нарушены не будут. Все эти проверки снижают количество необходимых тестов.
Re[10]: [Зависимые типы] Объясните на пальцах.
От:
Аноним
Дата:
03.07.09 11:26
Оценка:
Здравствуйте, dotneter, Вы писали:
D>Здравствуйте, SergH, Вы писали:
SH>>Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п. D>Даже для D>
D>sum x y = x + y
D>
D>?
А если в спецификации было написано "реализовать функцию вычитания целых чисел с именем sub"?
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, SergH, Вы писали:
SH>>Баг это отличие программы от спецификации. Или отличие спецификации от "того, что имелось ввиду". Имея на руках только программу ни то ни другое доказать невозможно. Если есть формальная спецификация, по которой можно что-то доказывать, то скорее всего её можно формально и преобразовать в программу, т.е. "формальная спецификация" это программа и есть. Осталась только разница между спецификацией и мечтой, и вот она видимо неустранима и соответствие не доказать.
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>либо не компилируется, либо гарантированно возвращает отсортированное.
А можно ли потом такой передать как обычный список в другую функцию? Будет неявное реобразование типа? Потребуется ли явное преобразование или может еще какие операции?
Здравствуйте, SergH, Вы писали:
SH>Для доказательства нужно формально сравнить "что хотелось" и "что получилось". Проблема в том, что "что хотелось" в формальном виде отсутствует.
sum x:int y:int — хочется Х (Х — спецификация оператора +)
получилась реализация
sum x:int y:int = x + y
которая эквивалентна операции + которая по определению является правильной, следовательно sum удовлетворяет тому что хотелось и является правильной.
Здравствуйте, dotneter, Вы писали:
D>sum x:int y:int — хочется Х (Х — спецификация оператора +)
Это ты сейчас думаешь, что тебе этого хочется Это может оказать заблуждением. Вдруг тебе понадобится искусственное переполнение на границе 2^32, для совместимости с С-библиотекой?
Здравствуйте, gandjustas, Вы писали:
G>Здравствуйте, thesz, Вы писали:
T>>Для зависимых типов не нужен запуск программы. Для контрактов нужен.
G>Неправда.
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>А можно ли потом такой передать как обычный список в другую функцию? Будет неявное реобразование типа? Потребуется ли явное преобразование или может еще какие операции?
Список с доказательством имеет структуру, аналогичную обычному списку. Все доказательства изъяты на момент компиляции.
Поэтому, несмотря на "необходимость преобразований", расходы будут нулевыми.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Здравствуйте, gandjustas, Вы писали:
G>>Здравствуйте, thesz, Вы писали:
T>>>Для зависимых типов не нужен запуск программы. Для контрактов нужен.
G>>Неправда.
T>http://rsdn.ru/forum/philosophy/3395836.1.aspx
Это может оказать заблуждением. Вдруг тебе понадобится искусственное переполнение на границе 2^32, для совместимости с С-библиотекой? 
