OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Четверг, 17 Октябрь, 2019 08:24

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 10 ] 
Автор Сообщение
 Заголовок сообщения: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 09:49 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Лиспоподобный язык для системных задач, был разработан для написания на нём верифицированных ядер операционных систем.

Цитата:
BitC is a new systems programming language. It seeks to combine the flexibility, safety, and richness of Standard ML or Haskell with the low-level expressiveness of C.

Цитата:
As a litmus test, it is possible to write a MPEG decoder or SHA-1 hash algorithm in BitC that is fully safe, but performs competatively with the C implementation. Today, that can't be done in SML, O'Caml, or Haskell.


Автор языка -- Jonathan Shapiro, год назад уходя из своего универа в Майкрософт, собирался забросить BitC, но сейчас собрался вернуться и с новыми силами взяться за этот язык.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 12:37 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 818
Откуда: Казань
Geniepro писал(а):
Лиспоподобный язык для системных задач, был разработан для написания на нём верифицированных ядер операционных систем.

Хотелось бы узнать как делается верификация для функциональных языков. Читал, что верификация для функциональных языков делается достаточно просто, но сам метод верификации не видел. Может кто-нибудь просто и доступно объяснить как оно делается или же дать ссылку, где хорошо объяснено?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 14:00 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Начинать, наверное, надо с изучения литературы по таким языкам, как Coq, Agda2, тот же BitC. К сожалению, на русском такую доходчивую информацию я не видел.
"The Algebra of Programming" вроде как фундаментальна в этом плане, правда, говорят, трудное чтиво...


Вложения:
Комментарий к файлу: The Algebra of Programming (Prentice-Hall International Series in Computer Science)
Richard Bird, Oege de Moor

Describes an algebraic approach to programming that permits the calculation of programs. Introduces the fundamentals of algebra for programming. Presents paradigms and strategies of program construction that form the core of Algorithm Design. Discusses functions and categories; applications; relations and allegories; datatypes; recursive programs, optimization issues, thinning algorithms, dynamic programming and greedy algorithms. Appropriate for all programmers.

aop.djvu [1.71 МБ]
Скачиваний: 130
Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 14:02 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9147
Откуда: Россия, Орёл
Суть любой верификации в том, что описание в одной формальной модели-нотации представляется параллельно в другой, с доказательством эквивалентности. Например, программа и вывод в предикатах; или формальная спецификация - и построенная по ней программа на ФЯ.

Суть не в самой формалистике (в ней всегда "не суть"), а в том, что совершить одну и ту же ошибку и в одной форме, и в другой - очень маловероятно.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 14:40 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 818
Откуда: Казань
Geniepro писал(а):
Начинать, наверное, надо с изучения литературы по таким языкам, как Coq, Agda2, тот же BitC. К сожалению, на русском такую доходчивую информацию я не видел.
"The Algebra of Programming" вроде как фундаментальна в этом плане, правда, говорят, трудное чтиво...

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 15:10 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Rifat писал(а):
Вот примерно так хотелось бы получить в нескольких словах общую идею верификации программ на функциональных языках.

Не, ну если в нескольких словах, то примерно так же и в ФП...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 15:24 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 818
Откуда: Казань
Тогда может лучше указать различия. Инварианта цикла скорее всего не будет, так как в функциональных языках обычно не бывает циклов. Как обходятся без инварианта цикла? Что используют вместо него?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 15:51 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Rifat писал(а):
Тогда может лучше указать различия. Инварианта цикла скорее всего не будет, так как в функциональных языках обычно не бывает циклов. Как обходятся без инварианта цикла? Что используют вместо него?

Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Пятница, 19 Март, 2010 16:57 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 530
Откуда: Москва
Geniepro писал(а):
Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.
А Вы его хоть раз делали? Только честно :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: The BitC Programming Language
СообщениеДобавлено: Понедельник, 22 Март, 2010 12:51 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Peter Almazov писал(а):
Geniepro писал(а):
Будет не инвариант цикла, а индуктивное доказательство корректности рекурсивной функции.
А Вы его хоть раз делали? Только честно :)

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

В ФЯ рекурсий не так уж и много -- композиция функций позволяет обходиться без рекурсий. map/fold/filter/zip -- и не надо никаких рекурсий...


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 10 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2019, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB