[isabelle-dev] ADTs in Scala
nipkow at in.tum.de
Mon Apr 16 17:07:41 CEST 2012
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev