Это немного расплывчатый вопрос, но я попробую.
Неоднородные среды
Работа сериализации состоит в том, чтобы брать данные из памяти одной компьютерной программы, преобразовывать их в какое-то стандартизированное представление и преобразовывать их обратно в данные в памяти, вполне возможно, другой компьютерной программы на совершенно другом компьютере. Это открывает некоторые интересные возможности.
Например, представление значения с плавающей запятой на многих компьютерах — IEEE754. Но это не совсем универсально; исторически такие компании, как Cray и IBM, использовали альтернативные форматы, поэтому существует вероятность того, что значение при десериализации на этих машинах может не совпадать с тем же значением, которое было сериализовано изначально. Обычно это никого не волнует, потому что численные различия очень малы.
Это проявляется в некоторых технологиях сериализации; Собственные проводные форматы ASN.1 для поплавков представляют собой либо текстовое представление, либо собственный двоичный формат, отличный от IEEE754. Идея текстового представления заключается в том, что оно может передавать любое значение с плавающей запятой без каких-либо ограничений. Напротив, двоичный формат часто имеет ограничения по точности, максимальному значению и т. д.
Текст — еще одна потенциальная проблемная область; сериализованные строки Unicode, отправленные на другой компьютер, который не поддерживает Unicode, скорее всего, приведут к тому, что десериализованная строка будет отличаться от исходной.
Точно так же с платформами, которые не поддерживают 64-битные целые числа и т. д. Java очень раздражает - исторически у нее не было целых чисел без знака, поэтому обработка 64-битных значений без знака, полученных, скажем, из программы на C++, доставляет неудобства.
Вывод: это логически невозможно
Таким образом, в некотором смысле, для гетерогенных сред не может быть технологий сериализации, формально доказанных, что они воспроизводят идентичные значения, потому что целевая машина имеет другую архитектуру, и ее представление вполне может быть другим или каким-то образом ограниченным.
Однородные среды
Сериализация, используемая для передачи данных из компьютерной программы на одном компьютере в точно такую же программу на идентичном компьютере (то есть в однородной среде), должна давать точно такие же значения при десериализации. Насколько я знаю, формально проверенных технологий сериализации не существует. Если в язык Ada встроена сериализация (я не знаю), то компилятор Greenhills Ada формально доказан. Boost for C++ тщательно рецензируется экспертами, поэтому он близок, особенно если используется поверх официально проверенного компилятора Greenhill C++ и имеет библиотеку сериализации. Некоторые из коммерческих инструментов/библиотек ASN.1 являются очень зрелыми и пользуются большим доверием.
Что формально доказано?
В последнем абзаце я коснулся трудности с вашим вопросом; формальное доказательство, возможно, имеет значение только в том случае, если весь стек разработки программного обеспечения (библиотеки, компилятор, ЦП) и исходный код вашего приложения сами формально подтверждены. В противном случае у вас мог бы быть идеальный исходный код для библиотеки сериализации, скомпилированной мусорным компилятором, связанной с мусорными библиотеками, работающей на низком процессоре; это не сработает.
Таким образом, когда говорят о «формально доказанных», обычно говорят о системе в целом, а не только об отдельном компоненте. Компонентная часть, соответствие которой формально доказано, сама по себе является хорошим подспорьем в создании проверенной системы, но сама по себе она не придает волшебным образом «правильности» всей системе. Каждый другой компонент также должен соответствовать спецификации.
Исторически мы видели, что довольно часто процессоры на самом деле не делают того, что указано в их технических характеристиках. Некоторые будут использовать ярлыки в арифметике с плавающей запятой в интересах выполнения инструкций за один цикл, а не для достижения численно идеального результата.
Извините за бессвязный ответ, но я надеюсь, что это интересно и поможет.
person
bazza
schedule
26.06.2019
