Thank you. I'm not familiar with his work. But will be soon ;-)
On Sun, Mar 7, 2010 at 5:49 AM, Felix Holmgren <[email protected]>wrote: > I wonder if people in this discussion have studied the work on hidden > algebra, by the late Joseph Goguen. This includes techniques for > automatic reasoning about stateful systems and other systems that are > otherwise hard to study formally: > > "Hidden algebra effectively handles the most troubling features of > large systems, including concurrency, distribution, nondeterminism, > and local states, as well as the usual features of the object > paradigm, including classes, subclasses (inheritance), attributes and > methods. . . The hidden algebra approach takes as basic the notion of > observational abstraction, or more precisely, behavioral satisfaction: > this means that hidden specifications characterize how objects (and > systems) behave in response to a given set of experiments, rather than > how they are implemented. . . induction is used to establish > properties of data types; while coinduction is used to establish > (behavioral) properties of objects with states." > > The logical backing for most of this uses category theory which, as > you know, has a lot in common with graph theory. > > There are implementations of these techniques, for example the BOBJ system: > > http://cseweb.ucsd.edu/groups/tatami/bobj/ > > There are examples there for how to prove properties of systems with > hidden states. > > There was also work on an extension for Maude called "Behavioral > Maude" by Grigore Rosu. There are several papers on this, and I seem > to remember that the extension could be downloaded but can find it > now. > (His related Circ tool is available here: > http://fsl.cs.uiuc.edu/index.php/Circ) > > Maude is in the tradition of a series of systems developed by Joseph > Goguen and others. To me (a non-expert), Goguen was one of the most > inspiring persons in Computer Science. Many people might associate him > with Formal Methods, which perhaps are not the latest craze among > VPRIers, but his work was very much geared towards creating tools that > were useful to actual programmers. He was also very interested in > human-computer interface issues, and, among other things, he was the > first editor of the influential Journal of Consciousness Studies. (And > yes, early on he worked on formalizations of General Systems Theory.) > > (Also look up "From OBJ to Maude and Beyond" by José Meseguer, a > relatively recent paper that looks at some of the achievements of OBJ > and it extensions, and how they can be implemented in Maude.) > > Personally, like most people here is suspect, I regard Smalltalk and > its descendants as the most vital innovations in practical computing > in the last decades, and I sympathize with those who feel that Formal > Methods leads down a track where a real programmer can't get much work > done. Still, I hope that ideas from the OBJ-tradition can come to mix > with the Smalltalk (and Lisp) traditions. > > /Felix > > > > 2010/3/6 John Zabroski <[email protected]> > > > > Ah, your welcome -- but I like your explanation even better. It is much > more condensed and shorter. > > > > On Fri, Mar 5, 2010 at 7:46 PM, Alejandro Garcia <[email protected]> > wrote: > >> > >> > >> On Fri, Mar 5, 2010 at 7:20 PM, Alejandro Garcia <[email protected]> > wrote: > >>>> > >>>> Thanks John for showing math for states. > >>>> Andrey this is what I mean when I say sytem B has only two states: > >>>> (quoting myself a hundred emails ago) > >>>> """ > >>>> In the image each (circle) is a simple machine that: > >>>> a) Can have just two values true or false. > >>>> b) if it gets an input it just sets that input as its value and > forwards it. > >>>> If the arrows are connected by an arc means logical AND > >>>> if the arrows are not connected and they arrive to the same node it > means logical OR. > >>>> """ > >>>> Given that we can see how the system will behave: > >>> > >> > >> > >> "If we set this to True" > >> > >> "It has a ripple effect on the other notes" > >> > >> "system B behaves as if it was just one circle" > >> > >> > >> > >>> > >>> > >>>> > >>>> By the way the original image is taken from the Necessary & Sufficient > series from Goldratt. > >>>> > >>>> On Fri, Mar 5, 2010 at 5:21 PM, John Zabroski <[email protected]> > wrote: > >>>>> > >>>>> > >>>>> On Fri, Mar 5, 2010 at 4:04 PM, Andrey Fedorov <[email protected]> > wrote: > >>>>>> > >>>>>> > >>>>>> Are those numbers you derived from the picture alone? If you did, > could you go through the math? Unless I'm misunderstanding the notation > (could you link to a rigorous definition?), I see System B having a lot more > than 2 states. > >>>>>> > >>>>> > >>>>> This has to do with observable characteristics of systems, and is an > argument laid down by model checking gurus as well as object capability > security gurus. > >>>>> > >>>>> The high-level idea is that you can make checking correctness or > limiting authority by limiting the state-surface of the program, by design. > >>>>> > >>>>> Say you have two pennies. Each penny has two states. Each penny > being flipped is independent of the other penny. 2 x 2 = 4 states. > >>>>> > >>>>> Now add a penny. 2 x 2 x 2 = 8 states. > >>>>> > >>>>> Add another penny > >>>>> > >>>>> 2 x 2 x 2 x 2 = 16 states > >>>>> > >>>>> Add another > >>>>> > >>>>> 2 x 2 x 2 x 2 x 2 = 32 states > >>>>> > >>>>> Add 2 more > >>>>> > >>>>> 2 x 2 x 2 x 2 x 2 x 2 x 2 = 128 states. > >>>>> > >>>>> Now suppose you enclose 128 possible states by 'fixing' certain > tosses of each coin so that they end up always heads or always tails. In > short, applying an Adapter pattern. > >>>>> > >>>>> Let's bias 4 coins. > >>>>> > >>>>> 1 x 1 x 1 x 1 x 2 x 2 x 2 = 8 states > >>>>> > >>>>> We've reduced the complexity of the system by an order of magnitude. > But what if we biased the wrong coins to always be heads or always be > tails? Now we've got a 'maintenance problem'. > >>>>> > >>>>> But,,, what if you can use this order of magnitude change in a more > positive light? > >>>>> > >>>>> Maybe the above 8 state configuration can have 4 coins be either > heads or tails, and we want to allow for toggling between all heads or all > tails. > >>>>> > >>>>> Well, that's > >>>>> > >>>>> 8 + 8 = 16 states. > >>>>> > >>>>> Now the only real problem with this sort of complexity analysis using > states is distribution (feedback and redundancy) and openness > (extensibility). > >>>>> > >>>>> However, one application of this basic way of managing complexity has > to do with defining systems into partitioned subsystems, and subcontracting > those systems out to various bidders. This allows the bidding process for a > software project to include more than just one bid proposal from IBM, > Because individual bid proposals don't have to be 1,000+ page bid documents > that only IBM can afford to pay typewriter monkeys to stack together. > > _______________________________________________ > fonc mailing list > [email protected] > http://vpri.org/mailman/listinfo/fonc >
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
