Если про SPARK, то здесь приводил парочку.
Жаль, что с какого-то момента — некоторые цитаты всё-таки в google придётся искать Ж-( Sorry / виноват, каюсь
В оправдание: реально где-то в правилах было, что внешние URL не приветствуются
)
этим и хорош Си — понятно, во что он транслируется.
Так и Modula-2 понятно во что. Идёшь step by step в Topspeed отладчике и Assembler изучаешь Ж-) ( в отдельном под-окошке)
continue и break — это goto
Да ( в точности так же, как и исключения см. далее )
if вместе с for — тоже goto
а вот и нет Ж-)
Ведь борьба Э.Дейкстра &Co с Goto началась для того,
что бы программу можно было читать сверху вниз
( без бесконечной перемотки полотна распечатки)
и доказывать блок за блоком её верность
Сам по себе GoTo на уровне машинных кодов никому не мешал и не мешает
Поэтому: моё «это же goto» просто читаем как «делает программу сильно не очевидной» Ж-)
P.S. Break активно использовал при обработке событий — без него можно, но как-то совсем уж мутно Ж-)
Вот теория и практика — расходятся Ж-)
( про ЛГУ: признаюсь честно Ж-) не помню читал или нет
M-2 в СССР был довольно популярен, про комп-р MAРC толи в Правде ( или в Известиях), толи в Н&Ж были статьи на весь разворот и т.д.)
Про железо — можно пруф?
Я собственно, считал, что про Н.Вирта, как практика,
уж Ж-) настолько часто упоминают, что можно и полунамёком Ж-)
Просто напишу, где лично я про это читал
Собственно ( про M-2 в Союзе см.ниже) про то, что Н.Вирт начиная с Modula-2 делал ещё HW + OS «к языку» есть во всех его биографиях ( пару URL далее)
Про Lilith впервые прочитал в книге Н.Вирта «Программирование на языке Модула-2» ( в предисловии). Издательство «Мир», кажется.
«Мир» печатал классику неплохими тиражами.
Книги были даже в публичной библиотеке Заводского района ( кстати, это и оф.название Ж-) )
Брайан Керниган, известный популяризатор языка Си, соавтор классического руководства по Си (K&R), написал критическую статью «Почему Паскаль не является моим любимым языком программирования»
Ремарка: её, кстати, «завернули» из журнала IEEE ещё при рецензировании
( лучше сразу укажу, что пишу по памяти: журнал «наикрутейший» точно,
c названием «могу допустить неточность» Ж-) )
... 2 апреля 1981 г., т.е. через два года (!) после реализации группой Вирта в ETH первого компилятора Modula-2 и через год после выпуска аппаратной реализации Modula-2 — персонального компьютера Lilith.
Выходит, за дело: вместо сравнения с «доведённым» до практического применения языка ( из крупного: AZ/400 до перевода «на объекты» и C++) сравнивали с «академическим» прародителем
P.P.S. Только сегодня сопоставил даты: раньше казалось, что Б.К. просто имел мало шансов узнать про новости из Швейцарии
P.P.P.S. Статья классическая и критика её тоже «всем известна»
Да, да и есть целая профессия — спец-ы по заполнению налоговых деклараций
Сейчас и в СНГ решили её «внедрить»: принимают законы об ответственности такий спе-ов
Как раз не-математиков и любят мучать Паскалем ( хорошо если не Basic-ом, причём тем что с нумерацией строк)
добрый друг подарил мне Кернигана и Ритчи «Язык программирования C».
А мне вот подарили тоненькую книгу зелёно-белую.
Во второй половине — штуки три новеллы Э.Дейкстры и ещё парочку про социальную ответственность программиста...
P.S. вот он как социализм людей не так ориентировал Ж-)
Иначе страшновато, например, за ответственные применения:
Сейсмоподвеска гостиницы «Казахстан» в Алматы, уникальное по тем временам сооружение в 10-балльной зоне, была спроектирована как дипломная работа моим преподавателем по термеху. Весь их выпуск работал над этим фактически, то есть реально можно было взять диплом выпускника кафедры сопромата и по этому диплому строить уникальное здание.
native support for floating-point arithmetic recently added in the SMT-LIB standard. Our approach is implemented in the Why3 environment and its front-end SPARK 2014 for the development of safety-critical Ada programs
Computer-aided verification of computer programs often uses SMT solvers. A common technique is to translate preconditions, postconditions, loop conditions, and assertions into SMT formulas in order to determine if all properties can hold.
There are also many verifiers built on top of the Alt-Ergo SMT solver. Here is a list of mature applications:
•Why3, a platform for deductive program verification, uses Alt-Ergo as its main prover;
•SPARK, uses CVC4 and Alt-Ergo (behind GNATprove) to automate the verification of some assertions in SPARK 2014;
Symbolic-execution based analysis and testing
An important application of SMT solvers is symbolic execution for analysis and testing of programs...
P.S. Забавно, там и Си есть:
•CAVEAT, a C-verifier developed by CEA and used by Airbus; Alt-Ergo was included in the qualification DO-178C of one of its recent aircraft;
•Frama-C, a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins (dedicated to «deductive program verification»);
Ну не любят за океаном «дедушку Вирта».
Есть версия, что мешал ( и мешает) делать «плясь плясь и в» кассу Ж-)
( это из «получен аванс — полный успех проекта»)
Если про SPARK, то здесь приводил парочку.
Жаль, что с какого-то момента — некоторые цитаты всё-таки в google придётся искать Ж-( Sorry / виноват, каюсь
В оправдание: реально где-то в правилах было, что внешние URL не приветствуются
)
Так и Modula-2 понятно во что. Идёшь step by step в Topspeed отладчике и Assembler изучаешь Ж-) ( в отдельном под-окошке)
Да ( в точности так же, как и исключения см. далее )
а вот и нет Ж-)
Ведь борьба Э.Дейкстра &Co с Goto началась для того,
что бы программу можно было читать сверху вниз
( без бесконечной перемотки полотна распечатки)
и доказывать блок за блоком её верность
Сам по себе GoTo на уровне машинных кодов никому не мешал и не мешает
Поэтому: моё «это же goto» просто читаем как «делает программу сильно не очевидной» Ж-)
P.S. Break активно использовал при обработке событий — без него можно, но как-то совсем уж мутно Ж-)
Вот теория и практика — расходятся Ж-)
Писал здесь про модули в Си и включение их в стандарт
Так вот их все ждут для ускорения компиляции
( сейчас .h приходится обрабатывать для каждого include)
а в M-2/ADA/TP уже из коробки модули и ускорение компиляции больших проектов
P.S. потому и в Си хотят, но не... Ж-)
Совместимость мешает
а чаще всего — сбой «железа».
Delphi или нет в прикладном ПО не влияет
P.S. Хотя, есть ведь OS и на ADA. Говорят, что аки «крест животворящий» демонов синеэкранных изгоняет Ж-) ( на 3 дублированом HW, включая RAM)
M-2 в СССР был довольно популярен, про комп-р MAРC толи в Правде ( или в Известиях), толи в Н&Ж были статьи на весь разворот и т.д.)
Я собственно, считал, что про Н.Вирта, как практика,
уж Ж-) настолько часто упоминают, что можно и полунамёком Ж-)
Просто напишу, где лично я про это читал
Собственно ( про M-2 в Союзе см.ниже) про то, что Н.Вирт начиная с Modula-2 делал ещё HW + OS «к языку» есть во всех его биографиях ( пару URL далее)
Про Lilith впервые прочитал в книге Н.Вирта «Программирование на языке Модула-2» ( в предисловии). Издательство «Мир», кажется.
«Мир» печатал классику неплохими тиражами.
Книги были даже в публичной библиотеке Заводского района ( кстати, это и оф.название Ж-) )
Никлаус Вирт в Академгородке
Там же про Modula-2 в СССР и в РФ
P.S.
Ещё биография + факт говорящий:
Никлаус Вирт — патриарх надежного программирования
Ремарка: её, кстати, «завернули» из журнала IEEE ещё при рецензировании
( лучше сразу укажу, что пишу по памяти: журнал «наикрутейший» точно,
c названием «могу допустить неточность» Ж-) )
Выходит, за дело: вместо сравнения с «доведённым» до практического применения языка ( из крупного: AZ/400 до перевода «на объекты» и C++) сравнивали с «академическим» прародителем
P.P.S. Только сегодня сопоставил даты: раньше казалось, что Б.К. просто имел мало шансов узнать про новости из Швейцарии
P.P.P.S. Статья классическая и критика её тоже «всем известна»
Сейчас и в СНГ решили её «внедрить»: принимают законы об ответственности такий спе-ов
Боинг — на ADA, ИЛ-96 ( по слухам) — тоже
P.S. На Си, говорят, тоже можно
надо только макрос «eq» завести
и в if-ах сперва цифру потом eq потом переменную
P.P.S. И что только не придумывают «только бы не строить дороги» Ж-)
P.P.P.S. Ми-6 + Ми-26 Ж-)
Проблема в одном — Delphi, действительно, не чистый Паскаль
В Free Pascal есть штук 5 разновидностей опции компилятора ( или даже несколько семейств опций)
какому из Borland диалектов соответствовать
Т.е. на практике TP изучен вдоль и поперёк разработчиками компиляторов
А мне вот подарили тоненькую книгу зелёно-белую.
Во второй половине — штуки три новеллы Э.Дейкстры и ещё парочку про социальную ответственность программиста...
P.S. вот он как социализм людей не так ориентировал Ж-)
В Pascal, кстати, есть вложенные процедуры ( в Си — нет) тоже может помочь
Иначе страшновато, например, за ответственные применения:
Таки есть и для Mac OS :-)
Кросс-компилятор точно был и отладка шла как раз на отдельном(?) комп-е с Маком
а вот ещё какое не то производство начнут программировать — страшно Ж-)
В принципе не удастся Ж-) Там числа сравнимые с числом атомов в пол-вселенной — комп-р не построить Ж-)
Для тестирование можно взять числа около нуля, единицы, в начале и конце каждого значения экпоненты,
плюс минус единица, максимум, минимум
А SPARK, надеюсь, «доказывает теоремы» как в высшей математике Ж-):
Automating the Verification of Floating-Point Programs
и
Satisfiability modulo theories
P.S. Забавно, там и Си есть:
Забавно, что многое как раз из free проекта взяли в «платный» Delphi ( вполне официально, ещё и пожертвование от фирмы внесли)
Есть версия, что мешал ( и мешает) делать «плясь плясь и в» кассу Ж-)
( это из «получен аванс — полный успех проекта»)