----- Mensaje original ----- De: David Abrahams <dave@boost-consulting.com> Fecha: Lunes, Septiembre 12, 2005 11:06 pm Asunto: Re: [boost] [serialization] No Reply?
* You should find some way to describe what it means for an input and an output archive to be compatible. Try to do that as formally as possible. You may have to rely on the fuzzy C++ notion of "equivalence," but I wouldn't blame you for that.
IMHO, there's no need to go fuzzy or rely on an undefined notion of "equivalence" between a serialized object and its restored copy. One can define these concepts with much precision in an "operational semantics" way, much as, for instance, semantics of logic languages is formally defined: * A type T is serializable if the expressions oar<<ct; iar>>t; are valid, where ct is of type const T& and t is of type T&, oar is an output archive and iar is an input archive. * The storage sequence, or simply storage, of an output archive oar is the ordered sequence of *all* calls s(i) of the form: oar<<out(i); where out(i) is of type const T(i)&. * Given an output archive oar with storage s(i) such that every T(i) is serializable, we say that an input archive iar is associated to oar if the sequence of expressions iar>>in(i); where in(i) is of type T(i)&, does not throw. We assume the input sequence ranges over the entire lifetime of iar. * Under the assumptions above, we say that in(i) is a restored copy of out(i). This defines association between archives in an abstract way. We can go concrete on a per archive basis, for instance: * Given an text output archive oar dumping to a file ofl, and an text input archive iar reading from a file if, iar is associated to oar if the contents of ifl coincide with those of ofl. Now that we have defined what it means for an input archive to be associated to an output archive, we can define the operational semantics of serialization from the concept "being a restored copy". In what follows we use the previous notation. The idea is to begin with primitive types and build on those. * If in(i) is of type bool&, in(i)==true if and only if out(i)==true. * If in(i) is of type char&, the numerical value of in(i) is that of out(i). * Similarly for other integral types. Different word sizes should be taken into account. * If in(i) is of type T*&, and T is serializable, *in(i) is a restored copy of *out(i). We can extend this schema inductively as we progress to more complex types. For example: * If in(i) is of type std::vector<T>&, and T is serializable, then in(i).size()==out(i).size() and each in(i)[j] is a restored copy of out(i)[j]. IMHO, this is sufficiently formal and solves two theoretical issues: * We have defined association between output and input archives without mentioning extralinguistical devices (files, network streams, and so on.) * We have a satisfactory definition of what serialization is supposed to do without relying on a naive "equivalence" relationship between objects and their restored copies: the main difficulty of such a naive approach like for instance "the restored copy has the same value as the original object", is that it does not mean much when these objects belong to different programs, running on different timeframes and perhaphs on different platforms. What do you think? Admittedly, what I've written still has some edges to rough, but I think it is sound enough. Joaquín M López Muñoz Telefónica, Investigación y Desarrollo
This is quite interesting to me. Its going to take a little time to consider with the attention it deserves. Robert Ramey JOAQUIN LOPEZ MU?Z wrote:
----- Mensaje original ----- De: David Abrahams <dave@boost-consulting.com> Fecha: Lunes, Septiembre 12, 2005 11:06 pm Asunto: Re: [boost] [serialization] No Reply?
* You should find some way to describe what it means for an input and an output archive to be compatible. Try to do that as formally as possible. You may have to rely on the fuzzy C++ notion of "equivalence," but I wouldn't blame you for that.
IMHO, there's no need to go fuzzy or rely on an undefined notion of "equivalence" between a serialized object and its restored copy. One can define these concepts with much precision in an "operational semantics" way, much as, for instance, semantics of logic languages is formally defined:
* A type T is serializable if the expressions oar<<ct; iar>>t; are valid, where ct is of type const T& and t is of type T&, oar is an output archive and iar is an input archive.
The above doesn't seem right to me. I don't see its necessary here an it makes the concept of serializable and archive circular. I believe that the inductive definition below - and currently in the document (more or less) defines the concept of serializable well enough.
* The storage sequence, or simply storage, of an output archive oar is the ordered sequence of *all* calls s(i) of the form: oar<<out(i); where out(i) is of type const T(i)&.
* Given an output archive oar with storage s(i) such that every T(i) is serializable, we say that an input archive iar is associated to oar if the sequence of expressions iar>>in(i); where in(i) is of type T(i)&, does not throw. We assume the input sequence ranges over the entire lifetime of iar.
* Under the assumptions above, we say that in(i) is a restored copy of out(i).
This defines association between archives in an abstract way. We can go concrete on a per archive basis, for instance:
* Given an text output archive oar dumping to a file ofl, and an text input archive iar reading from a file if, iar is associated to oar if the contents of ifl coincide with those of ofl.
Now that we have defined what it means for an input archive to be associated to an output archive, we can define the operational semantics of serialization from the concept "being a restored copy". In what follows we use the previous notation. The idea is to begin with primitive types and build on those.
* If in(i) is of type bool&, in(i)==true if and only if out(i)==true. * If in(i) is of type char&, the numerical value of in(i) is that of out(i). * Similarly for other integral types. Different word sizes should be taken into account. * If in(i) is of type T*&, and T is serializable, *in(i) is a restored copy of *out(i).
We can extend this schema inductively as we progress to more complex types. For example:
* If in(i) is of type std::vector<T>&, and T is serializable, then in(i).size()==out(i).size() and each in(i)[j] is a restored copy of out(i)[j].
IMHO, this is sufficiently formal and solves two theoretical issues:
* We have defined association between output and input archives without mentioning extralinguistical devices (files, network streams, and so on.) * We have a satisfactory definition of what serialization is supposed to do without relying on a naive "equivalence" relationship between objects and their restored copies: the main difficulty of such a naive approach like for instance "the restored copy has the same value as the original object", is that it does not mean much when these objects belong to different programs, running on different timeframes and perhaphs on different platforms.
What do you think? Admittedly, what I've written still has some edges to rough, but I think it is sound enough.
Joaquín M López Muñoz Telefónica, Investigación y Desarrollo
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
participants (4)
-
JOAQUIN LOPEZ MU?Z -
Robert Ramey