On Mon, 16 Apr 2012, Holger Gast wrote:
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.
See
http://isabelle.in.tum.de/repos/isabelle/file/f4348634595b/src/Pure/General/graph.scala
for the concrete implementation we are speaking about. Maybe you want to
make a standard Java version from it -- with immutable objects, not
mutable ones.
"Immutable object" might sound like an oxymoron for OO according to 1995,
but it is commonplace in some leading edge communities. Immutability is
also the standard way in Isabelle/Scala (and Isabelle/ML) to get clean
semantics and good performance in a parallel setting.
BTW, this thread emerged from another one about the JUNG framework, where
graphs are mutable according to some old standard patterns. This meant
one had to clone the whole thing occasionally in the usual awkward way.
The new graph.scala avoids all this extra overhead, and also the
dependency of the huge JUNG framework.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
