В С++ тоже, но не сразу

@true_grue Спасибо за наводку на CompCert, я про него то ли не знал, то ли забыл. Полистал исходники — у меня сложилось впечатление, что там вполне себе классический lexer-hack (Lexer.mll мудрит с таблицей символов и решает, какой токен вернуть парсеру: VAR_NAME, TYPEDEF_NAME или OTHER_NAME), но я не углублялся. А так-то да, альтернативы lexer-hack-у есть, об одной из них я писал выше — парсить "обобщённую" КС-грамматику, а потом разбираться в parse tree с узлами типа "объявление переменной или выражение".

Не только. Даже "A<B>C;" — это либо объявление переменной, либо выражение в С/С++ в зависимости от kind-а A.

Т.е. тоже неоднозначность, где используют lexer-hack и т.п.

Там два прохода делается. Первый — в pre_parser.mly. Посмотрите здесь раздел 5 Experimentation on a C99 Parser: https://link.springer.com/content/pdf/10.1007/978-3-642-28869-2_20.pdf

А, ну понятно тогда, зачем там два парсера, для ocamlyacc и для menhir. Спасибо.

Я так понимаю проблема в том что легаси от си, была уже кодобаза для сишных компиляторов и ранних компиляторов си с классами, оттуда была взята эта составная лексема, и выпилить её было не так уж просто в дальнейшем. А шарпы язык более молодой, поэтому разработчики уже знали что их ждёт такой подвох

емнип там просто добавили это как исключительный случай

Только в этом случае нужно еще учитывать, что оператор сдвига не может содержать в себе пробелы.

Детальный разбор почему верификация плавающей арифметики бесполезная трата сил если конечно заранее не известно для какого процессора и какого компилятора (включая флаги) это делается:

https://hal.archives-ouvertes.fr/file/index/docid/281429/filename/floating-point-article.pdf

Я не очень понимаю такие расплывчатые утверждения в статьях по верификации: A first objection to this practise (проверять x на неравенство нулю) is that, any-way, computing 1/x for x very close to zero will generate very large numbers that will most probably result in overflows later.

А верификация интервальной арифметики? Posit, в частности?

However, as weshowed in§3.1.1, on x87 a comparison may be performed on extended precision operands, which may later be rounded to lesser precisions depending on registers pills. We showed in the preceding section that this particularity made some proof methods unsound, and it also makes the above bound unsound. In order to be sound, we should use the predoperation on the extended precision type; but then, because of possible rounding to lesser precisions, we should round the bounds of the interval... which would bring us back to abstracting < as we abstract ≤

Ну и если у вас soft floats или любая другая арифметика полностью написанная на ALU то все намного проще конечно же

Интервальную арифметику считают и на "аппаратных" FPU:
уставливаем режим "округление вниз", считаем.

Потом "вверх".

В итоге получаем [ min .. max ] интервал.

Причём этот интервал подчиняется законам "чистой математики".

Т.е. это уже не "IEEE-тика".

И вот именно ПО в стиле Pascal XSC и имеет смысл верифицировать / доказывать правильность программы.

И как это решит аппаратный нон-детерминизм? Когда деление или извлечение корня на разном оборудовании может давать несколько разный результат? Ну и если конечно рассматривать только один компилятор вроде паскаля то это проще, но тот же LLVM довольно фривольно обращается с плавающей арифметикой даже без ffast-math

Есть предложение:

_заставить_ производителей "железа" соблюдать стандарты.

Хотя бы, IEEE.

--

Про "non детерминизм" - там же не задействован датчик случайных чисел?

Значит, всё вполне детерминировано, т.е. воспроизводимо.

( а бардак с "гайками и болтами" с шагом резьбы "не по ГОСТу" решается, скажем так, "юридически ми методами". Ничто не ново под луной.)

Например AMD использует Goldschmidt division на аппаратном уровне а Intel - Newton–Raphson division. И IEEE никак не регламентирует как это должно быть реалищзовано на аппаратном уровне

А то как разные CPU обрабатывают субнормальные числа это вообще отдельная история

И? В интервальной арифметике просто результирующий интервал станет шире.

(  а если не станет, то значит, что и.а. в конкретной аппаратуре реализована неправильно)