Оберон-технология: особенности и перспективы |
Тематика обсуждения: Оберон-технология. Особенности, перспективы, практическое применение.
Всего в теме 6256 сообщений
Добавить свое сообщение
Отслеживать это обсуждение Обсуждение из раздела Школа ОБЕРОНА
№ 5366 02-10-2007 04:30 | |
№ 5365 02-10-2007 04:20 | |
Ответ на »сообщение 5361« (Geniepro)
___________________________
Так что кому надо - верифицировать могут без особых проблем, другое дело, что на языках вроде Хаскелла, когда программа большей частью состоит из декларативных утверждений, сама надобность в верификации кода не так остра, как в ФП - сама програама наглядно показывает, что она делает (каким должен быть результат), так что верификация в основном выявляет мелкие ошибки типа опечаток да ошибок при редком рефакторинге... И ещё очень помогает удостоверению в правильности программ сам процесс написания функций с параллельным их тестированием, о котором часто упоминали функциональщики...
Справедливости ради, картина не так идеальна. Необходимость доказательства завершимости еще никто не отменял, как и halting problem. Например (псевдокод):
factorial(0) = 1
factorial(n) = n * factorial(n-1) Представим на минутку, что функция не столь тривиальна.
Кроме того, часто верифицировать все же приходится систему в целом, а не отдельные функции. Скажем, приведенный выше пример становится корректным, если задать в спецификации предусловие n >= 0 и все вызывающие функции верифицировать относительно выполнения этого предусловия.
Тем не менее, с точки зрения верификации ФЯ выглядят очень перспективно, поскольку их конструкции ближе к тому математическому аппарату, который применяется при верификации реальных программ. Слабейшие предусловия Дейкстры "по жизни" начинают дополнять временнЫми логиками, эффектами, монадами (да, именно) и тому подобными штуками.
№ 5364 02-10-2007 03:45 | |
>>> О тестах видимо ни в Госте, ни данный господин не слышали.
Слышали, батюшка.
Только пользуемся книжечками с правленными страницами этих самых ГОСТов,
в которых ляп на ляпе. Зато своего рода ноу хау.
А ведь обязательная к исполнению вещь!
И когда эти глупости увеличены ФЯ с его неизмеримой мощью - это страшно неудобно!
Кстати, текст из Matematica 2.2 не всасывается в Matematica 10. А где взять 2.2?
А смысл текста программы не понятен для среднего императивного ума.
Читать его должны нормальные инженеры!
№ 5363 02-10-2007 03:23 | |
Ну вот, Jack! Сами предлагали надысь не гнать лошадей, а у Вашей - пена с губ!
Каюсь, некстати, "верификация" ввернул. У Вас (и не только) это нечто особенное.
Как говорили латиняне говорить надо не так, чтобы поняли, а так, чтобы не могли не понять.
Есть правильные программы и программы, которые соответствуют задаче.
Разницу понимаете?
Сами говорили, что в ФЯ программа на себя берёт массу рутинной работы, не давая программисту
ошибиться в этой части.
Но тем самым в ФЯ меньше контакта с требухой программы и, соответственно,
меньше контроля за исполнением.
В случае, если есть подозрение, что правильная программа решает по сути не ту задачу,
то выяснение происхождения ошибки в представляется на основании этих аргументов
в ФЯ более трудным, чем в ИЯ. Что не так?
По поводу контроля сложности. Процитирую сам себя:
"управление сложностью больших систем - это та же ручная работа".
Обратите внимание - "та же". То есть та же, что и в Обероне, например.
Нету тут ни плюса у ФЯ, ни серебра.
>>> каким образом механизмы управления сложностью, находящиеся ВНЕ языка программирования
>>> не могут быть по каким то принципиальным причинам применены к ДРУГОМУ языку программирования
По принципиальным - могут, а вот по конкретным (например, маргинальной нише языка) - могут и не.
Например для Си и Паскаля есть широко доступные системы, а для ... но тпру! ... стоять, Гнедая!
Дело здесь в создании именно внеязыковой системы. Своего рода IDE, но не типа текстовой редактор
плюс компилятор, а нечто, позволяющее удобно и эффективно работать со сложными структурами.
№ 5362 02-10-2007 03:19 | |
Ответ на »сообщение 5361« (Geniepro)
___________________________
сама надобность в верификации кода не так остра, как в ФП
имелось в виду "как в ИП"
№ 5361 02-10-2007 03:16 | |
Ответ на »сообщение 5356« (Как слышно? Приём!)
___________________________
Короче - в ФЯ затруднительно провести ручную верификацию.
Ну... Хм, а зачем Вам ручная верификация?
Jack Of Shadows как-то приводил здесь ссылку на работу, в которой описывалась разработка верифицированного микроядра ОС seL4 семейства L4. Там микроядро было написано на Хаскелле, затем его верифицировали с помощью утилиты (theorem proover) Isabelle, затем переписали на С++.
Также аналогичный пример - микроядро Timber - тоже написали на диалекте Хаскелла, верифицировали и переписали на Си для ускорения работы...
Так что кому надо - верифицировать могут без особых проблем, другое дело, что на языках вроде Хаскелла, когда программа большей частью состоит из декларативных утверждений, сама надобность в верификации кода не так остра, как в ФП - сама програама наглядно показывает, что она делает (каким должен быть результат), так что верификация в основном выявляет мелкие ошибки типа опечаток да ошибок при редком рефакторинге... И ещё очень помогает удостоверению в правильности программ сам процесс написания функций с параллельным их тестированием, о котором часто упоминали функциональщики...
№ 5360 02-10-2007 02:23 | |
Ответ на »сообщение 5359« (Beginner)
___________________________
Может речь о проверке на листочке бумаге с карандашом?
А математики по вашему как работают ? А ведь императизьму у них ни в одном глазу :))
№ 5359 02-10-2007 02:13 | |
Ответ на »сообщение 5357« (Jack Of Shadows)
___________________________
Может речь о проверке на листочке бумаге с карандашом? Кто-то из авторитетов такой критерий предлагал. Я тоже наступал на грабли с отечественными ГОСТ.
№ 5358 02-10-2007 01:58 | |
Ответ на »сообщение 5356« (Как слышно? Приём!)
___________________________
Если целиковую задачу ФЯ разруливает самостоятельно, то комбинация из подпрограмм, работа с библиотеками, управление сложностью больших систем - это та же ручная работа.
То есть весь накопленный в этой области опыт на императивных языках, при переходе на функциональный язык волшебным образом улетучивается ?
Все то что накопила индустрия в области управления сложными проектами - к ФП почему то неприменимо ?
Я не понимаю каким образом механизмы управления сложностью, находящиеся ВНЕ языка программирования не могут быть по каким то принципиальным причинам применены к ДРУГОМУ языку программирования, даже функциональному.
Или может быть вы говорите о механихмах управления сложностью, В САМОМ языке программирования. В таком случае озвучьте их. Что же это за недоступные ФП программистам механизьмы такие ?
№ 5357 02-10-2007 01:53 | |
Ответ на »сообщение 5356« (Как слышно? Приём!)
___________________________
Пройти пошагово методом ИП невозможно.
Соответственно, нет возможности удостовериться в сомнительном отсутствии ошибок.
Круто. Здесь часто звучала мысль, что для оберона дебагер (пошаговая отладка) не нужен, потому как видите ли ПРАВИЛЬНЫЙ язык, и программы на нем ПРАВИЛЬНЫЕ пишутся :))
А вот данный господин тут считает что дебагер (пошаговая отладка) это необходимый просто верификатор (афигеть!!) надежности императивных программ. О тестах видимо ни в Госте, ни данный господин не слышали.
Я видал разные обвинения в адрес ФП во многих грехах. Но вот в верифицируемости программ (!!! одной из самых сильных сторон функционального подхода) слышу в первый раз.
Остается только поразиться каким же образом работает скажем компилятор GHC. Ведь по мнению "Как слышно? Приём!" проверить, да еще и ПОШАГОВО (sic!!) его невозможно. Да и вообще его же ЦЕЛИКОМ понимать надо! Это ж ФУНКЦИОНАЛЬНАЯ едрить ее программа! :))
Добавить свое сообщение
Отслеживать это обсуждение
Дополнительная навигация: |
|