Так опять же, это не значит, что тесты вас спасут. Там ведь может быть ровно та же ситуация.
Я и не утверждаю, что тесты спасут. Моё утверждение состояло в том, что действительно надёжное ПО можно получить путём верификации и тестирования, они взаимно дополняют друг друга. Безусловно, полной гарантии не будет, но это существенно лучше, чем только тестирование или только верификация.
К счастью, идея всех этих инструментов в том, что людям не нужно вникать в доказательства. Достаточно посмотреть на тип функции (то есть, на утверждение теоремы).
Это замечательно, но опять же, как я понял, это для функционального программирования. Увы, оно не единственное. И не ослабевающий интерес в виде научных конференций и публикаций именно по дедуктивной верификации императивных программ это лишь подтверждает.
Не знаю.
Вооот. А я именно про императивные программы писал. Возможно, это было не очевидно изначально — приношу извинения. Верификацией функциональных программ я не занимался, но ведь наверняка там тоже не всё гладко в плане полной (или максимально полной) автоматизации.
Я же не ругаю инструмент, который Вы использовали. Я в некоторой степени попытался примирить горячих спорщиков «тестирование vs верификация» в комментариях.
И? Ошибки могут быть везде. Поэтому всё относительно, и верификация тоже. Напишите неверную спецификацию, она случайно подойдёт к программе и получите некорректную программу.
Но ведь это и не нужно: ведь достаточно лишь того, что тайпчекинг (то есть, proof verification) разрешим, разве нет?
Конечно недостаточно. Даже в учебных примерах по дедуктивной верификации императивных программ вылазят такие громоздкие формулы, что мои студенты, по-моему, мимо ушей пропускают идею доказательства. Что говорить о реальных программах.
Функциональщики это решают известно как: вам не нужно думать об инвариантах цикла, если у вас нет циклов.
Это, конечно, замечательно, но как быть с императивными программами?
Так для этих систем типов выполняется свойство строгой нормализации, поэтому любая корректно типизированная функция завершима и тотальна.
«Для этих» — для ситуации с разворачиванием списка? Ну так я вроде не только про этот частный случай отвечал изначально. Задача останова, как известно, алгоритмически не разрешима (в общем случае). Я этой проблемой не занимаюсь, но бывал на лекциях про инструменты типа Terminator и Slam — то есть для каких-то частных случаев что-то сделать можно.
Автору моё глубочайшее уважение. Однако я не программист, а математик :)
В комментариях все по-своему правы. Верификация тоже не панацея: есть переделка процитированного утверждения Дейкстры. Что-то в духе «верификация способна доказать отсутствие ошибок в программе, но не всегда доказывает их присутствие». Проблема тут в спецификации: а если ошибка в ней, а не в программе? И это ещё не все проблемы верификации: невозможность полной автоматизации, проблема генерации инвариантов циклов, задача исследования завершимости…
Поэтому если говорить не о маленьких примерах типа разобранного в статье (для которого вполне достаточно верификации), то если мы хотим действительно получить надёжное ПО, нужно применять и верификацию, и тестирование.
При проверке постусловия не анализируется что происходит в теле функции. Просто проверяется предикат с теми значениями, которые получились при выходе из функции.
Так в итоге, для примера выше — компилятор поймёт, что n не 7, а 6 при выходе из функции?
Стандарт не накладывает на компиляторы обязанность проверять корректность всей программы по контрактам. И программист может не описывать контракты для вообще всех функций в программе. Это допустимо. Но если всё же все контракты описаны, то проверить программу по логике Хоара возможно. Но не с помощью компилятора.
И в чём тогда польза? Не вижу тогда принципиального отличия от банального перебора различных значений параметров функции и возвращаемых значений.
Я как раз имел ввиду, что в контракте хотим, чтобы n == 7 (постусловие), но в теле через указатель присваиваем 6. Вот и хочу понять, как компилятор определит, что контракт не выполнен.
Задача компилятора просто проверить соблюдение контракта для каждой отдельно взятой функции
Так вот что это значит — «проверить соблюдение контракта»? Вы имеете ввиду для каждого конкретного вызова с конкретными значениями параметров? Ну тогда тут логика Хоара вообще не при чём.
Несколько замечаний:
1. Логика Хоара позволяет доказывать не корректность алгоритма, а корректность программы. Это важно. Например, существует не один алгоритм сортировки массивов, пред- и постусловия у каждой конкретной реализации будут совпадать, только вот инварианты циклов и условия корректности будут существенно отличаться (как следствие, их доказательство).
2. Возможность проводить анализ частичной корректности программы (то есть соответствие её спецификации — «контрактам» в описываемой терминологии) существует достаточно давно: достаточно вспомнить проект VCC. Есть даже плагин для MS Visual Studio.
3. Совершенно неясен вопрос с семантикой. Например, как моделируется память?
[[ expects: n == 5 ]]
[[ ensures n: n == 7 ]]
{
int n;
int *p = &n;
*p = 6;
}
В данном примере в контрактах побочных эффектов нет. Что будет в результате обработки данного кода?
4. Без инвариантов циклов всё это будет более-менее работать только в безцикловых программах (фрагментах программ). Причём автоматически породить инвариант цикла невозможно (в общем случае). И если пред- и постусловие программист в общем-то, думаю, в состоянии написать (или довести до ума в процессе отладки), то вот с инвариантами циклов не всё так просто. Причём чем выше уровень вложенности цикла, тем задача становится сложнее.
5. Ещё про семантику: как реально компилятор будет проверять соблюдение контрактов? Нужна семантика, чтобы порождать условия корректности, а потом их доказывать. С автоматическим доказательством в общем виде тоже всё плохо. В уже упомянутом VCC идёт связка с Z3 (SMT-решатель), но и тот не бог.
В целом начинание хорошее и полезное, хотя очевидно, что программисты к этому не готовы. Но в любом деле в начале всегда трудности. Спасибо за статью.
Я и не утверждаю, что тесты спасут. Моё утверждение состояло в том, что действительно надёжное ПО можно получить путём верификации и тестирования, они взаимно дополняют друг друга. Безусловно, полной гарантии не будет, но это существенно лучше, чем только тестирование или только верификация.
Это замечательно, но опять же, как я понял, это для функционального программирования. Увы, оно не единственное. И не ослабевающий интерес в виде научных конференций и публикаций именно по дедуктивной верификации императивных программ это лишь подтверждает.
Вооот. А я именно про императивные программы писал. Возможно, это было не очевидно изначально — приношу извинения. Верификацией функциональных программ я не занимался, но ведь наверняка там тоже не всё гладко в плане полной (или максимально полной) автоматизации.
Я же не ругаю инструмент, который Вы использовали. Я в некоторой степени попытался примирить горячих спорщиков «тестирование vs верификация» в комментариях.
И? Ошибки могут быть везде. Поэтому всё относительно, и верификация тоже. Напишите неверную спецификацию, она случайно подойдёт к программе и получите некорректную программу.
Конечно недостаточно. Даже в учебных примерах по дедуктивной верификации императивных программ вылазят такие громоздкие формулы, что мои студенты, по-моему, мимо ушей пропускают идею доказательства. Что говорить о реальных программах.
Это, конечно, замечательно, но как быть с императивными программами?
«Для этих» — для ситуации с разворачиванием списка? Ну так я вроде не только про этот частный случай отвечал изначально. Задача останова, как известно, алгоритмически не разрешима (в общем случае). Я этой проблемой не занимаюсь, но бывал на лекциях про инструменты типа Terminator и Slam — то есть для каких-то частных случаев что-то сделать можно.
В комментариях все по-своему правы. Верификация тоже не панацея: есть переделка процитированного утверждения Дейкстры. Что-то в духе «верификация способна доказать отсутствие ошибок в программе, но не всегда доказывает их присутствие». Проблема тут в спецификации: а если ошибка в ней, а не в программе? И это ещё не все проблемы верификации: невозможность полной автоматизации, проблема генерации инвариантов циклов, задача исследования завершимости…
Поэтому если говорить не о маленьких примерах типа разобранного в статье (для которого вполне достаточно верификации), то если мы хотим действительно получить надёжное ПО, нужно применять и верификацию, и тестирование.
Так в итоге, для примера выше — компилятор поймёт, что n не 7, а 6 при выходе из функции?
И в чём тогда польза? Не вижу тогда принципиального отличия от банального перебора различных значений параметров функции и возвращаемых значений.
Так вот что это значит — «проверить соблюдение контракта»? Вы имеете ввиду для каждого конкретного вызова с конкретными значениями параметров? Ну тогда тут логика Хоара вообще не при чём.
1. Логика Хоара позволяет доказывать не корректность алгоритма, а корректность программы. Это важно. Например, существует не один алгоритм сортировки массивов, пред- и постусловия у каждой конкретной реализации будут совпадать, только вот инварианты циклов и условия корректности будут существенно отличаться (как следствие, их доказательство).
2. Возможность проводить анализ частичной корректности программы (то есть соответствие её спецификации — «контрактам» в описываемой терминологии) существует достаточно давно: достаточно вспомнить проект VCC. Есть даже плагин для MS Visual Studio.
3. Совершенно неясен вопрос с семантикой. Например, как моделируется память?
[[ expects: n == 5 ]]
[[ ensures n: n == 7 ]]
{
int n;
int *p = &n;
*p = 6;
}
В данном примере в контрактах побочных эффектов нет. Что будет в результате обработки данного кода?
4. Без инвариантов циклов всё это будет более-менее работать только в безцикловых программах (фрагментах программ). Причём автоматически породить инвариант цикла невозможно (в общем случае). И если пред- и постусловие программист в общем-то, думаю, в состоянии написать (или довести до ума в процессе отладки), то вот с инвариантами циклов не всё так просто. Причём чем выше уровень вложенности цикла, тем задача становится сложнее.
5. Ещё про семантику: как реально компилятор будет проверять соблюдение контрактов? Нужна семантика, чтобы порождать условия корректности, а потом их доказывать. С автоматическим доказательством в общем виде тоже всё плохо. В уже упомянутом VCC идёт связка с Z3 (SMT-решатель), но и тот не бог.
В целом начинание хорошее и полезное, хотя очевидно, что программисты к этому не готовы. Но в любом деле в начале всегда трудности. Спасибо за статью.