May I remind the participants of this thread that this is the Isabelle development mailing list, not a discussion forum on OO techniques in general.
Thanks Tobias Am 16/04/2012 16:57, schrieb Holger Gast: >> b) Coding conventions and usual practice (my addition to the above): >> It is customary to make constructors, and not some auxiliary >> static methods, responsible for proper initialization. >> But this is exactly what did not work out smoothly. The task is to make >> an implementation of *immutable* datastructures. So you cannot just >> construct a new (empty) Graph and then invoke methods to update its state. >> You need to construct new graph objects from old ones in a manner that >> retains the intended semantics. > > The the aspect of being immutable or mutable is, of course, orthogonal of the > question of proper initialization: in either case, the construction in the > end must leave the object in a consistent state such that it can be used > further. Whether one uses the object thus created to > > a) modify the object's data as done in most current OO code > b) create new objects by calling constructors/static methods > c) create new objects by methods that produce new results > > is quite irrelevant here. > > In the current example of graphs, the issue of "consistency" > may not be so obvious, because it has a single field that by itself > is, of course, trivially consistent. > > -- > Holger > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
