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

[kpierre]

Цитата:

Потому, что «если»! Smile Если система верификации выдаёт положительную характеристику этой программе из трёх строк, то либо она справилась с проблемой Колатца, либо она не заметила, что программа может никогда не кончиться. В первом случае мы решили старую задачу в математике, во втором — система верификации не ловит один из серьёзных багов — зацикливание (т.е. слаба).

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

Цитата:

Как будем это верифицировать? (Лучшее известное мне определение систем реального времени звучит примерно так: «РВ: это когда ответ, не данный вовремя — неправильный ответ».) Каким образом мы будем доказывать, что программе хватит ресурсов (процессора, памяти… да мало ли чего)? Можно ли без подобного анализа говорить о готовности систем верификации для этой области применения?

Разумеется, построением мат. модели машины. Я вам уже приводил некоторые примеры.

Цитата:

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

Термин -- обыкновенный для любителей фп Вот например в википедии (http://en.wikipedia.org/wiki/Data_type):

Цитата:

A data type can also be thought of as a constraint placed upon the interpretation of data in a type system, describing representation, interpretation and structure of values or objects stored in computer memory. The type system uses data type information to check correctness of computer programs that access or manipulate the data.

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

[worm2]

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

Total FP может быть неплохим компромисом, особенно если удастся сделать практичный вариант.

А по-моему, это не компромисс а сдача без боя практики на милость теории
Я напомню, что в Total FP все операции должны быть определены на всех возможных значениях. Например, значение 1/0 должно быть определено и не должно приводить ни к каким исключительным ситуациям. Т.е. вместо того, чтобы доказывать, что значение знаменателя не может обратиться в нуль, Total FP предлагает нам: "ой, а я так не умею, давайте-ка лучше вы переопределите свою математику так, чтобы на ноль можно было делить, и вот тогда я вам всё докажу" И, по моему, хоть и дилетантскому, мнению, практичный вариант из этого сделать никогда не получится.

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

«РВ: это когда ответ, не данный вовремя — неправильный ответ»

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

[kpierre]

Цитата:

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

Да ладно, уже аж функцию аккермана написали

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

kpierre в сообщении #137586 писал(а):

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

Я бы назвал такой подход системой полуавтоматической верификации. Ну да ладно, проехали.

kpierre в сообщении #137586 писал(а):

Разумеется, построением мат. модели машины.

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

Мне это чем-то напоминает лапласовский детерменизм: может быть и можно, но непрактично. Статистическая механика работает лучше. А квантовая запрещает. Вопрос: а не упрёмся ли мы в подобный запрет.

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

kpierre в сообщении #137586 писал(а):

Цитата:

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

Термин -- обыкновенный для любителей фп Smile Вот например в википедии (http://en.wikipedia.org/wiki/Data_type):

Я имел в виду термин «строгая типизация». Я полагаю, Ваш ответ от другого вопроса.

В любом случае, что касается Вашего ответа: обычный для любителей ФП смысл — это хорошо, но мне кажется рискованным ожидать, что всё CS сообщество понимает тип также. Но даже если отвлечься от этого, к сожалению я не готов согласиться с «определением» ( это не определение, а мысли по поводу оного) Википедии. По сути оно совпадает с моим выше, с которым, я, как и было сказано, несколько не согласен. И по практическим, и по «философским» соображениям.

Что же касается множества значений, то я понимал его не в смысле теории множеств, а в смысле А-68 (именной типизации). То есть, я думаю, очень близко (если не тождественно) к ФП.

kpierre в сообщении #137673 писал(а):

Да ладно, уже аж функцию аккермана написали

А это — одна из самых популярных в практических приложениях функций!!!

Вопрос о практичности — ключевой вопрос в программировании, в отличии от Computer Science. Именно практичность отличает языки программирования от алгоритмических языков, учебных языков (типа Паскаля) и им подобных.

[kpierre]

Цитата:

Что же касается множества значений, то я понимал его не в смысле теории множеств, а в смысле А-68 (именной типизации). То есть, я думаю, очень близко (если не тождественно) к ФП.

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

Там даже в статье написано: "contrasts with structural systems, where comparisons are based on the structure of the types in question and do not require explicit declarations."

"Haskell, ML and Whiteoak are examples of structurally-typed languages."

Насколько я понял, structural проявляется в хаскеле в классах типов (Num a => ... -- я как раз выше приводил такой пример) и в полиморфизме (a -> Bool)

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

Цитата:

А это — одна из самых популярных в практических приложениях функций!!! Laughing

Вот кстати, объяснение почему она весьма важна: http://dxdy.ru/topic10851.html#92740 Хотя, конечно, тот факт что далась она с трудом сам по себе смешон

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

kpierre в сообщении #137790 писал(а):

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

?!
Это как? Если есть и int, и long int, и для них определены одни и те же + - * /, то для меня не важно, какой использовать? Или Вы, кроме как об ошибках типа, ни о чём не думаете?

kpierre в сообщении #137790 писал(а):

Вот кстати, объяснение почему она весьма важна:

Гениально! Никогда не знал, что мне важно, примитивно ли рекурсивна функция, которую я написал.

Простите сарказм, но нельзя же так в самом деле: в моём сообщении «практических» было выделено и курсивом, и цветом. Ну да, для теории, для построения систем верификации это важно: это доказало, что TotalFP способен покрыть всё множество примитивно-рекурсивных функций плюс ещё плевок. Но практика это, в общем, не интересует. Утрируя, ему интересно две вещи: работатет ли то, что он написал, и может ли он что-либо взять в библиотеке и не писать сам. Ни в первый, ни во второй случай ф.А. обычно не попадает.

Конечно, хорошо, что почти всё, что я пишу, примитивно рекурсивно. Но я вот прожил столько лет, и не знал, что говорю прозой. Так и здесь: меня этот факт просто не волнует. Более того, эта аналогия мне нравится всё больше: прозой способны говорить все, хорошей прозой и стихами — литераторы. Многие из нас читают с удовольствием, но пишут единицы. Не так ли и с верификацией и ФП: они должны базироваться на нуждах практики, иначе индустрия их не примет. Что вовсе не мешает существовать высокой литературе и высоким теориям, а мне — наслаждаться книгами.

[kpierre]

Цитата:

Это как? Если есть и int, и long int, и для них определены одни и те же + - * /, то для меня не важно, какой использовать? Или Вы, кроме как об ошибках типа, ни о чём не думаете?

Вы тут говорите о неявном полиморфизме "/" и "*". Не уверен, что на алголе можно написать аналогичные произвольные ф-ции. А в остальном да -- типы существуют чтоб не было ошибок, вы не знали?

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

kpierre в сообщении #137890 писал(а):

Вы тут говорите о неявном полиморфизме

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

kpierre в сообщении #137890 писал(а):

А в остальном да -- типы существуют чтоб не было ошибок, вы не знали?

Я не знал. Более того, Вам на слово не поверю. Так что, по-прежнему не знаю.

Лично я всегда считал, что для предотвращения ошибок служат не типы, а проверка типов. Что не одно и тоже. Ср.: спорт и проверка на допинг.

[kpierre]

Цитата:

Я не знал. Более того, Вам на слово не поверю. Так что, по-прежнему не знаю.

Лично я всегда считал, что для предотвращения ошибок служат не типы, а проверка типов. Что не одно и тоже. Ср.: спорт и проверка на допинг.

Согласен, что я выразился совершенно некорректно -- имелось в виду следующее: я могу в бестиповом языке эмулировать все св-ва типов кроме проверки типов.

Правда, я и сам уже начал в этом сомневаться

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

Мне кажется, что типы — это один из инструментов описания семантики программы. Строгость системы типизации — это, в некотором смысле, уровень формальности этого инструмента. Практика требует ослабления формальности (из разных соображений), но неформальный подход ведёт к случаям «потери взаимопонимания» между автором программы и компьютером–исполнителем (каковую ситуацию и называют ошибкой типизации). Отсюда и поиск приемлемого компромиса.

[e2e4]

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

:evil:

e2e4 в сообщении #137242 писал(а):

Если не секрет, поделитесь как Вы определяли фазу и частоту сигнала? ДПФ или что-то другое?

Подробно рассказать не могу, но грубо так: поскольку частота сигнала примерно известна (50 Гц держат довольно точно), то можно сравнивать сигнал $S$ с эталоном $S_0$ (и подсчитать $S \times \bar{S_0}$). Тогда мы имеем фазу, а скорость вращения фазы позволяет уточнить частоту эталона. Дальше уже точно не мои секреты полишинеля.

Т.е. некоторый программный вариант ФАПЧ. А что за операция, обозначенная Вами как $\times$? Умножение векторов?

[ha]

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

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

ha в сообщении #142447 писал(а):

Программы без ошибок, в некотором смысле, бывают

см. (и далее).

ha в сообщении #142447 писал(а):

Решения с ошибками там проходят все тесты очень редко.

Какое симпатичное определение программы без ошибок (шучу, шучу!).

[вв]

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

:evil:
Есть три аксиомы Шура-Бура:...

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