Rambler's Top100
"Knowledge itself is power"
F.Bacon
Поиск | Карта сайта | Помощь | О проекте | ТТХ  
 Базарная площадь
  
О разделе

Основная страница

Группы обсуждений


Тематический каталог обсуждений

Архив

 
 К н и г и
 
Книжная полка
 
 
Библиотека
 
  
  
 


Поиск
 
Поиск по КС
Поиск в статьях
Яndex© + Google©
Поиск книг

 
  
Тематический каталог
Все манускрипты

 
  
Карта VCL
ОШИБКИ
Сообщения системы

 
Форумы
 
Круглый стол
Новые вопросы

 
  
Базарная площадь
Городская площадь

 
   
С Л С

 
Летопись
 
Королевские Хроники
Рыцарский Зал
Глас народа!

 
  
ТТХ
Конкурсы
Королевская клюква

 
Разделы
 
Hello, World!
Лицей

Квинтана

 
  
Сокровищница
Подземелье Магов
Подводные камни
Свитки

 
  
Школа ОБЕРОНА

 
  
Арсенальная башня
Фолианты
Полигон

 
  
Книга Песка
Дальние земли

 
  
АРХИВЫ

 
 

Сейчас на сайте присутствуют:
 
  
 
Во Флориде и в Королевстве сейчас  12:35[Войти] | [Зарегистрироваться]
Обсуждение темы:
Оберон-технология: особенности и перспективы


Тематика обсуждения: Оберон-технология. Особенности, перспективы, практическое применение. 

Количество сообщений на странице

Порядок сортировки сообщений
Новое сообщение вверху списка (сетевая хронология)
Первое сообщение вверху списка (обычная хронология)

Перейти на конкретную страницу по номеру


Всего в теме 6256 сообщений

Добавить свое сообщение

Отслеживать это обсуждение

Обсуждение из раздела
Школа ОБЕРОНА

<<<... | 5376—5367 | 5366—5357 | 5356—5347 | ...>>>
Всего сообщений в теме: 6256; страниц: 626; текущая страница: 90


№ 5366   02-10-2007 04:30 Ответить на это сообщение Ответить на это сообщение с цитированием
Ответ на »сообщение 5354« (Руслан Богатырев)
___________________________

Ответ на »сообщение 5353« (qwerty)
___________________________

А можно поинтересоваться, какие сложные системы Вы проектировали/реализовывали на Обероне или на каком-либо другом языке? Или Вы занимаетесь только аналитикой и написанием статей?

Ответы на эти вопросы Вы можете найти по этим ссылкам:
http://rbogatyrev.livejournal.com/2007/05/31/
http://www.delphikingdom.ru/asp/talktopic.asp?ID=271&ref=msg&msg=2551#msg2551
http://rbogatyrev.livejournal.com/2007/07/17/

Спасибо. А что-нибудь из этого доступно в исходниках?


№ 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!!) его невозможно. Да и вообще его же ЦЕЛИКОМ понимать надо! Это ж ФУНКЦИОНАЛЬНАЯ едрить ее программа! :))


<<<... | 5376—5367 | 5366—5357 | 5356—5347 | ...>>>
Всего сообщений в теме: 6256; страниц: 626; текущая страница: 90


Добавить свое сообщение

Отслеживать это обсуждение

Дополнительная навигация:
Количество сообщений на странице

Порядок сортировки сообщений
Новое сообщение вверху списка (сетевая хронология)
Первое сообщение вверху списка (обычная хронология)

Перейти на конкретную страницу по номеру
  
Время на сайте: GMT минус 5 часов

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

Web hosting for this web site provided by DotNetPark (ASP.NET, SharePoint, MS SQL hosting)  
Software for IIS, Hyper-V, MS SQL. Tools for Windows server administrators. Server migration utilities  

 
© При использовании любых материалов «Королевства Delphi» необходимо указывать источник информации. Перепечатка авторских статей возможна только при согласии всех авторов и администрации сайта.
Все используемые на сайте торговые марки являются собственностью их производителей.

Яндекс цитирования