Обещание json.flang «разбор печати даёт то же значение» ложно, и ломается оно тремя разными способами
Шапка flang/stdlib/json.flang обещает: «печать выводит его без изменений, и разбор печати даёт то же значение». У «Напечатать строку json» то же сказано сильнее: «Что обещается и что проверено корпусом — тождество на ЗНАЧЕНИИ: разбор напечатанного даёт ровно то значение, которое печатали». Проверка кругом «печать → разбор → печать» ломает это тремя входами, и все три — следствия решений, названных в той же шапке.
| значение, собранное руками | круг даёт |
|---|---|
| объект с двумя полями «а» (1 и 2) | {"а":2} — дубль ключа съеден разбором |
«Число json» с величиной 0 делить на 0 | НЕ РАЗОБРАНО: неизвестный знак: N — печать выдаёт NaN, а это не JSON вовсе |
| «Текст json» со знаком кода 1 | "\\\u0001" вместо "\u0001" — печать даёт \u0001, разбор его НЕ раскрывает, и второй круг заслоняет обратную косую |
Первый вход — прямое следствие «решения второго» (дубли ключей схлопываются), второй и третий — «решения первого» (\uXXXX проверяется, но не раскрывается). То есть обещание противоречит соседним абзацам той же шапки.
Обещание верно с оговоркой, и оговорки в тексте нет. Круг держится для значений, ПРИШЕДШИХ ИЗ РАЗБОРА: у них не бывает ни дублей ключей (разбор их уже схлопнул), ни не-числа (грамматика JSON его не принимает), ни сырых управляющих знаков (они уже разложены). Корпус состоит ровно из таких значений — поэтому он обещание и не опроверг. Значение, собранное программой руками, ни одного из этих свойств не имеет.
Чему учит. Обещание, проверенное корпусом, проверено на том подмножестве входов, которое корпус умеет породить. Если корпус порождает значения ОДНИМ путём (разбором текста), он не скажет ничего про значения, приходящие ДРУГИМ путём (сборкой в программе), — а именно вторым путём они и приходят у всякого, кто библиотекой пользуется.
Чем подтверждено. Ветка vypusk/utv-http на основании github/main df055a6b, двоичный из bootstrap/. Круг замкнут через строку восьмистрочной функцией «Печать итога» в пробнике (значения сравнить нельзя, см. соседнюю заметку); все три строки таблицы — вывод flang check, а не рассуждение.
Чем ограничено. Проверено тринадцатью значениями, не фаззингом. Четвёртого способа сломать круг не искали.
Связано: round-trip-claims-are-unstatable-in-postconditions, proven-is-not-correct, byte-for-byte-comparison