Программа без ошибок - такая же абстракция, как -273 градуса

[e2e4]

anonim писал(а):

Прототип функции выглядел как void func(char m[256]), а в самой функции было выражение типа sizeof(m).

Поэтому хорошей практикой является не указывать размер массива вовсе в прототипе функции - эта цифра никоим образом не учитывается компилятором. Для того, чтобы обозначить массив, лучше написать func(char m[]).

Кстати, еще похожий пример:

файл aaa.cpp:
char str[] = "abc";

файл bbb.cpp:
include "iostream.h"

extern int *str;
int main()
{
   cout<<str<<'\n';
}

Тот редкий случай, когда int a[] и int *a не взаимозаменяемы. Пример взят из книжки "Как не надо программировать на Си++", автора посмотрю чуть позже.

[AD]

e2e4 писал(а):

Пример взят из книжки "Как не надо программировать на Си++", автора посмотрю чуть позже

Стив Уэллин?

[e2e4]

AD писал(а):

Стив Уэллин

По моему, он.

Куда-то затерялась книга, поищу. Купил в ларьке типа "все за 40 руб" .

[Tarasov]

Добрый день!
Очень интересно было читать тему.

Хотел бы дать ссылку на одну любопытную статью http://kholeg.spaces.live.com/blog/cns! ... !152.entry

Заинтересовала тема "доказательного программирования". Предлагаю рассмотреть практический пример, хватит абстракций. Как, скажем, доказательно запрограммировать файловый сервер ftp ?

[незваный гость]

А что-нибудь попроще Вас не устроит? Например, алгорифм Евклида Вы готовы доказательно рассписать (здесь)?

Я не то, чтобы скептик. Как правило, никто не готов платить за доказательный код. Если Вы распишете а.Е., Вы увидите, насколько это трудоёмко.

[Tarasov]

незваный гость писал(а):

:evil:
А что-нибудь попроще Вас не устроит? Например, алгорифм Евклида Вы готовы доказательно рассписать (здесь)?

Я не то, чтобы скептик. Как правило, никто не готов платить за доказательный код. Если Вы распишете а.Е., Вы увидите, насколько это трудоёмко.

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

Видите ли, не вижу необходимости доказывать каждую строку программы. Когда дело касается какого-либо сложного алгоритма, разумеется правильность доказывать необходимо, но, насколько я понимаю, доказательство применяется именно к алгоритму, а не к коду.

Общий тезис: стремление к программам без ошибок с помощью лишь математики - тупиковый путь.

bak: Очень рад достижениям российских студентов на соревнованиях по программированию. Однако, к сожалению, мне не удалось ощутить наличие существования "русской школы программирования". Возможно потому что вуз не столичный =)

[незваный гость]

Tarasov писал(а):

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

То, что Вы не видите, не делает его бесполезным.

Tarasov писал(а):

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

Вы глубоко заблуждаетесь. Посмотрите Literate Programming, «Наука программирования» Д.Гриса, «Взаимодействие последовательных процессов» Хоара.

Более того, в некоторых областях (security, reliability) отладки быть не может: только by design.

Tarasov писал(а):

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

А зря.

Tarasov писал(а):

Когда дело касается какого-либо сложного алгоритма, разумеется правильность доказывать необходимо, но, насколько я понимаю, доказательство применяется именно к алгоритму, а не к коду.

Код — это формальная запись алгорифма. В чём Вы видите разницу?

Tarasov писал(а):

Общий тезис: стремление к программам без ошибок с помощью лишь математики - тупиковый путь.

А почему? Мне это успешно удавалось. Более того, когда я не знаю, как писать программу, я честно начинаю писать математику программы.

[Tarasov]

незваный гость писал(а):

Вы глубоко заблуждаетесь. Посмотрите Literate Programming, «Наука программирования» Д.Гриса, «Взаимодействие последовательных процессов» Хоара.

Возможно, заблуждаюсь.
Вы используете Literate Programming в своей деятельности? Обязательно займусь этой технологией. Насколько понял из описаний, это просто удобный способ работы с исходным текстом. А также развивает культуру документирования.

незваный гость писал(а):

Более того, в некоторых областях (security, reliability) отладки быть не может: только by design.

Как я понял, Вы отказываетесь от отладки как от некоего средства разработки, но не как от средства тестирования? Если это так, то я в чем то с Вами согласен. Однако считаю отладку чрезвычайно полезным инструментом, особенно для критических приложений. Например, при разработке программ для станков с программным управлением прежде всего обкатывают программу на симуляторе, и уже затем позволяют ей работать с заготовками.

незваный гость писал(а):

Код — это формальная запись алгорифма. В чём Вы видите разницу?

Разницу я вижу в том, что с точки зрения человека "Повторять пока i не больше нуля действие N" и

while(i<=0);
{
    N();
}

может оказаться одним и тем же.

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

незваный гость писал(а):

Tarasov писал(а):

Общий тезис: стремление к программам без ошибок с помощью лишь математики - тупиковый путь.

А почему? Мне это успешно удавалось. Более того, когда я не знаю, как писать программу, я честно начинаю писать математику программы.

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

[AD]

незваный гость писал(а):

:evil:
А что-нибудь попроще Вас не устроит? Например, алгорифм Евклида Вы готовы доказательно рассписать (здесь)?

Ух, что-то мы такое проходили ... инвариант цикла, ...

[e2e4]

незваный гость писал(а):

Например, алгорифм Евклида Вы готовы доказательно рассписать (здесь)

Д. Кнут, том1, "Основные алгоритмы" .

[незваный гость]

e2e4 писал(а):

Д. Кнут, том1, "Основные алгоритмы"

Что-то я не упомню такого. С расписанными пред- и пост-условиями, инвариантами циклов? Может, Вы более точно ссылку укажете?

Между прочим, алгорифм Евклида ещё пишут более или менее. А вот аккуратное выписывание двоичного поиска вызывает куда больше проблем. Я, не мудрствуя лукаво, сразу пишу предикаты. Поскольку по опыту знаю, что иначе совру.

Tarasov писал(а):

Разницу я вижу в том, что с точки зрения человека "Повторять пока i не больше нуля действие N" и
‹код›
может оказаться одним и тем же.

Ну так доказывайте правильность второго, кто ж Вам мешает?

Tarasov писал(а):

Т.е. в процессе трансляции кода с математического или иного алгоритмического языка на машинный язык (эту трансляцию выполняет человек) не исключены ошибки.

Не очень понял. Если речь идёт о С++, то доказывается именно правильность программы на С++. Если речь идёт о правильности трансляции С++ в машинный код, то её обычно выполняет не человек, а программа. И там, где это критично (в авиационном приборостроении, например), эта программа (компилятор) сама подлежит сертификации.

Tarasov писал(а):

Вы используете Literate Programming в своей деятельности?

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

Tarasov писал(а):

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

Принципа «разделяй и властвуй» ещё никто не отменял. А неучтённые моменты могут ловиться на assert'ах.

[worm2]

незваный гость писал(а):

Если речь идёт о С++, то доказывается именно правильность программы на С++. Если речь идёт о правильности трансляции С++ в машинный код, то её обычно выполняет не человек, а программа.

Вспомнилась Тьюринговская лекция Кена Томпсона: Размышления о том, можно ли полагаться на доверие.

[kpierre]

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

Добавлено спустя 1 час 50 минут 40 секунд:

Цитата:

Я не то, чтобы скептик. Как правило, никто не готов платить за доказательный код. Если Вы распишете а.Е., Вы увидите, насколько это трудоёмко.

Да, это трудоемко -- если доказывать код императивный. В случае строго типизированного (и, желательно, на функциональном яп) кода это совсем не сложно.

[незваный гость]

kpierre писал(а):

особенно если не считать ошибок смысловых.

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

kpierre писал(а):

Вобще-то "программа без ошибок" -- реальность

Я уже упоминал аксиомы Шура-Буры. Они не утверждают невозможности программы без ошибок, лишь ставят под сомнение её полезность.

kpierre писал(а):

Например, на языках с зависимыми типами (dependent types) можно написать программу сортировки

Это нехитро сделать и на C. Даже и на ассемблере. Вы вот контрол календаря напишите. Чтобы был интуитивно правильным. И, желательно, в стандартном Windows (без всех этих новомодных фрейворков. Почему? да потому, что фреймворки тоже люди пишут. Вот и поставьте себя на место фрейворкаписателя).

kpierre писал(а):

В случае строго типизированного (и, желательно, на функциональном яп) кода это совсем не сложно.

Возьмите Алгол-68 — академически формальная строгая типизация.

~~~

Я, боюсь, существую одновременно во множестве разных миров. В некоторых из них Вы правы: наверное, можно писать полезные программы на функциональных языках. В некоторых — нет. И даже не только потому, что найдите мне компилятор функционального языка, ориентированный на встроенные системы. Просто, когда речь идёт о строго хронометрированном опросе пары дюжин каналов с частотой 700 мкс и обработкой данных на процессоре с ограниченными ресурсами (скажем, PowerPC 20 МГц), на одном языке просто не получается писать. Начинаются всяческие разные вкрапления ассемблера, коды вспомогательных процессоров и подобные радости. И их тоже надо выписать без ошибок.

Есть и классическое определение ошибки в программе (Майерс, Искусство тестирования программ): ошибка — это когда программа делает не то, что ожидает пользователь. Соответственно, для доказательства правильности надо формализовать — а значит, необходимо огрубить, — пользователя. Что, в свою очередь, означает неминуемое внесение ошибок.

[kpierre]

Цитата:

Это нехитро сделать и на C. Даже и на ассемблере.

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

Цитата:

Вы вот контрол календаря напишите. Чтобы был интуитивно правильным. И, желательно, в стандартном Windows (без всех этих новомодных фрейворков. Почему? да потому, что фреймворки тоже люди пишут. Вот и поставьте себя на место фрейворкаписателя).

Никакой "контрол календаря" меня совершенно не интересует А уж windows -- тем более.

Цитата:

И даже не только потому, что найдите мне компилятор функционального языка, ориентированный на встроенные системы. Просто, когда речь идёт о строго хронометрированном опросе пары дюжин каналов с частотой 700 мкс и обработкой данных на процессоре с ограниченными ресурсами (скажем, PowerPC 20 МГц), на одном языке просто не получается писать. Начинаются всяческие разные вкрапления ассемблера, коды вспомогательных процессоров и подобные радости. И их тоже надо выписать без ошибок.

Такого компилятора нет, зато есть инструменты, позволяющие формально описывать многие встроенные системы вплоть до fpga и доказывать их корректность. И никто не собирается сами эти инструменты запускать на целевых системах.

Цитата:

Возьмите Алгол-68 — академически формальная строгая типизация.

Вот именно, что она только кажется строгой, на самом деле она там почти отсутствует

Цитата:

Есть и классическое определение ошибки в программе (Майерс, Искусство тестирования программ): ошибка — это когда программа делает не то, что ожидает пользователь.

Если добавить, "но то, что ожидает программист" -- тогда именно такие ошибки я и имел в виду, когда говорил "смысловые".

Добавлено спустя 5 минут 22 секунды:

Да, кстати, про

Цитата:

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

Доказательства корректности исходного кода этой системы, к примеру -- http://coq.inria.fr/ -- были произведены вручную. Поэтому нет повода не доверять тем д-вам и программам, что через нее прошли В основном она конечно не про программирование, а про доказательства, но опять же построена на зависимых типах и программировать кое-что можно.