[Javapathfinder-svn] SF.net SVN: javapathfinder:[1891] branches/mango/Mango/ javapathfinder-mango-bridge/mango/rewriter/MangoState.java

[<fra...@us...>]

Revision: 1891
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1891&view=rev
Author:   frankrimlinger
Date:     2009-09-04 14:34:30 +0000 (Fri, 04 Sep 2009)

Log Message:
-----------
Went a little overboard in 1890.  While it is true that the dual space of predicate transformers provides a sound theory for slicing and dicing control flow diagrams, this is only a means to and end.  The end is to interpret this dual graph as a specification.  This interpretation is in terms of the original concepts of predicate and state transformer.  In the particular case of a loop invocation along a edge, which started this thread, what happens is that "gates" are produced.  This is worth understanding.  Although a loop embedded in a control flow diagram has a single entry point, it might have many exit points.  When the loop collapses into the entrypoint, each such exit is represented with an edge containing the appropriate predicate transformer to encapsulate the last incomplete journey around the loop.  Having done this, we can now interpret the situation like so:

Any state which does not hang the loop must leave by one of the prescribed exits.  Therefore, the assumption of an exit condition is a specification for a set of states which do not hang the loop, because,evidently, they leave the loop along the prescribed edge.  Therefore, even if the recursive function for the state transition of the loop is not total, it is "good enough" for our purpose.

As a practical matter, the exit condition composes with the recursive function to get the weakest precondition at the entrance, and so it's really hard for the user to know what they are buying.  Therefore, such an assumption is referred to as a "conjecture", and the name of the game is for the user, or perhaps some robust ai process, to guess some hypotheses not involving the loop which imply the conjecture.  

In conclusion, it is not necessary for Step to maintain dual state, and so we have restored MangoState to 1884.  But this digression has raised one useful point.  When we assume a condition containing a recursive function, e.g., an instantiated loop, this is specified as a "conjecture", NOT a "hypothesis".  We have to stop and let the user try and guess some hypotheses which will imply the conjecture.  At some point, maybe atm will kick in to prove or disprove the conjectures.

If this part could be done automatically, then we truly would enter the realm of the "self-verifying compiler", but for now this is terra incognita.

Modified Paths:
--------------
    branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoState.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.