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
