Net!
++-Пример из жизни: продукт TCAS. Заказчик: FAA. Производитель: MITRE. Формальное доказательство корректности алгоритма - CSAIL (MIT). Сертификация - FAA. Жесткие требования ставятся к 1) корректности алгоритмов. 2) Соответствия кода алгоритмам. 3) применением сертифицированных операционной системы и инструментов разработки.++
Все правильно. И еще тестирование (многократно), и верификация и патчирование.
Только Вы контексте борта помянули некие 'закрытые коммерческие продукты'. И как оно вписывается? Их FAA сертифицирует?
АДА, которую в Rockwell-Collins пользуют, не на базаре в палатке куплена. ЭТОТ продукт создан специально и в FAA сертифицирован. Стандарт, в частности, и нужен для ЭТОЙ сертификации. Rockwell и FAA не одна лавочка. Там все по-взрослому и оооочень формально. Теперь ясно?
++ -Мнооого строчек кода ;-) И вам немного не повезло, я занимаюсь как раз проблемами оптимальной трансляции и формальной верификации кода. Так что задавайте ваши вопросы :) ++
Почему не повезло? Здесь часто бывают и серьезные оппоненты :-) , не только представители славного профессорско-преподавательского корпуса (я верно угадал?)
ЧтоВы хотите от Бейсика? Вы с радостным видом сообщили, что он таки еще и компилятор, а не только интертрепатор (как его тут весьма остроумно назвали). Я сказал, что это вроде и не новость даже, а Вы опять за билгейтство свое. В чем у нас по поводу Васика расхождение?
++Байт-код виртуальной машины++ -
Наша тема: ПО для борта. Зачем там Виртовы полеты фантазии?
++-Правильно, полезет. Вопрос лишь - надо ему туда лезть, или нет. Предположим, ваш массив набит единичками [сильное предположение, М.] и никто его не меняет[еще круче, М.]. Если компилятор сможет доказать факт его неизменности, то ему достаточно перемножить эти самые единички и в качестве исполняемого кода записать результат в левую часть присваивания. Догадались, что это будет тоже единичка? Т.е. в итоге одна операция записи константы на каждое число. [Это если исходить из предположения, что мы пишем такие программы, в которых одну и туже хрень надо два раза делать, М. (шутка ..)] Если же это Си, то ему еще нужно проверить, а не лезет ли кто ни будь в этот массив по абсолютной ссылке и не меняет-ли содержимое массива посредством прямого доступа в память. И если он этот факт доказать не сможет, то извиняйте, придется ему и в память лазать два раза, и единички перемножать.++
Давайте сразу, забыв на время о защите памяти, о кэше, подумаем о главном: откуда компилятор знает, что САМ он туда не влезал? Хранит адреса? Где хранит, какой объем хранилова? Тяжеловесная такая у Вас оптимизация получается, если конечно не единички множить.
++ Ага, хорошая школа, но ничего не гарантирует если студент лентяй. Я имел удовольствие интервьюировать PhD в области AI, как раз из MIT. Парень не смог мне объяснить разницу между дизъюнктивной и коньюнктиврой нормальными формами. Вас даже спрашивать не буду.++
Лентяй? В MIT?
Впрочем, я тоже не смогу ответить, сдал экзамен много лет назад, забыл сразу (а может и не знал вовсе, теперь уже не вспомнить : - ( ).
++Один, не допускающий неоднозначной трансляции исходного кода!!
- Простите меня, но неоднозначность трансляции определяется не стандартом, а 1) непротиворечивой грамматикой, 2) формально корректным оптимизатором, 3) формально корректным кодогенератором. Стандарт тут не причем, взгляните на курс компиляторов, не забыв при этом повторить конечные автоматы.++
А кто сомневался в том, что КОНКРЕТНЫЙ компилятор всегда однозначно компилит ОДИН иходный текст?
Вопрос в том, что если Вы в стандарте для некоего языка определите возможность использования указателей, ссылочных массивов, объектов и прочей радости то (да, трансляция, признаю, будет однозначной) исполняемый код будет обладать гораздо меньшей надежностью. У Вас винды висли? А программа в TCAS зависает?
Стандарт, в данном случае нужен, чтобы ограничить возможности языка. Что хорошо для хакера - плохо для борта.