Ada_Ru форум

Обсуждение языка Ада

Fw: [ada_ru] ????????????? ? ?????????? ????? ???

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

Сообщения

ksiby
Fw: [ada_ru] ????????????? ? ?????????? ????? ???
2009-09-03 11:19:03

 

День добрый!

 

 

With best regards

Sergey Kirkorov www.mediascan.by

Email: ksiby@...

 

----- Original Message ----- From: "Sergey Kirkorov" <ksiby@...>

To: "Vladimir Teplouhov" <vladimir.teplouhov@...>

Sent: Thursday, September 03, 2009 2:10 PM

Subject: Re: [ada_ru] Кодогенератор и компилятор языка Ада

Sergey Kirkorov wrote:

 

День добрый!

а для чего такое чудо, если не секрет?

Есть такая беда, как формальное доказательство правильности ПО. Сертификационные испытания по хорошему надо проводить начиная с инструментария иначе уровень доверия будет соответствовать наименьшему в этой цепочке (доверие как черному ящику) коим на мой взгляд и есть транслятор, сертифицированный на некоторое конечное множество тестов. Автоматизация формального доказательства правильности ПО для языка "С" топчется на уровне сотен операторов, если я не прав поправьте. В общем разбирают это все в лучшем случае полуавтоматически и стоит это очень больших денег.

Где это нужно? В общем случае редко где это является обязательным. В областях на которые позиционируется язык Ada -- практически везде если не обязательно то ОЧЕНЬ желательно.

 

Welcome to Open-DO!

 

http://forge.open-do.org/

 

PS. Open-DO: инициативный проект нескольких Европейских компаний по обмену опытом сертификации в соответствии со стандартом DO-178B. В том числе и разработки инструментальных средств поддержки этого проекта.

Возможно бутет полезно:

 

Есть еще такой себе компилятор Ada фирмы DDC-I

http://www.ddci.com/

SCORE чтоли. Они в свое время вложили немало в развитие технологии ANDF, TenDRA (http://www.info.uni-karlsruhe.de/~andf/index.htm).

 

Один из ранних анонсов:

http://www.info.uni-karlsruhe.de/~andf/ddci_ada95.htm

 

Другими словами их компилятор преобразует Аду в ANDF, затем ANDF в машинный код.

 

Так вот они же разработали формальныю спецификацию для ANDF используя математический аппарат action semantic

 

B. S. Hansen and J. U. Toft.

The formal specification of ANDF, an application of action semantics http://www.brics.dk/NS/94/1/BRICS-NS-94-1.pdf

 

Т.е. преобразовав Ада программу в ANDF можно

* ее дальше анализировать математическими методами

* можно компилить ее в код или интерпретировать с гарантией формальной корректности (см. например всякие "Actress: an action semantics directed compiler generator" http://eprints.kfupm.edu.sa/22683/)

Я с этим столкнулся изучая TenDRA в попытках написать свой компилятор Ada -> TDF(ANDF).

 

--

Maxim Reznik

Новое сообщение:
Страницы: 1

Чтобы оставить новое сообщение необходимо Зарегистрироваться и Войти