[Javapathfinder-svn] SF.net SVN: javapathfinder:[1832] branches/mango/Mango

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

Revision: 1832
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1832&view=rev
Author:   frankrimlinger
Date:     2009-08-16 19:18:06 +0000 (Sun, 16 Aug 2009)

Log Message:
-----------
Completed rebuild of specification for itsAWrap class.

Fixed wonderful typing bug, which illustrates the difference between <immutable> and <patternLiteral>.  Consider the predicate (= x y), where x and y are local variables.  Since x and y can represent any numbers, they certainly are not <immutable>.  Now look what happens when this starts to translate.  You might get an intermediate expression like (= "x" "y").  Well, it is tempting to think that "x" and "y" are <immutable>, since, after all, their values are unchanging.  So, you deduce that (tr (= "x" "y")) --> (tr 'f) --> "false".  Not a very satisfying deduction.  But what is really going on is that "x" and "y" are <patternLiteral>.  This means, as far as the unifier is concerned, these symbols appearing in a pattern could only match on themselves.  Clearly "x" doesn't *know* it represents a local variable x, and so cannot be expected to match on x.  However, like they say in traffic school, "ignorance is no excuse of the law".  You can't be <immutable> unless you know beyond a shadow of doubt that you correspond to only one physical object of the concrete Mango Model.  This is imaginary place where the *real* objects live, independent of any means of representing themselves.  Although it is imaginary, it is critical to imagine it accurately when answering questions of this nature.  As a rule of thumb:

<pattenLiteral>  is for syntax	EZ
<immutable>  is for semantics. TRICKY

In particular, a TranslationSym like "x" is <patternLiteral> but not <immutable>.  On the other hand, a ClassNameSym *is* <immutable>, because the JVM model, which lives inside Mango Model, tells us   that there is a unique class with any given name, so we are good-2-go in Mango Model world.

But applying this test to "x", here is what happens.  A local variable x which translates to "x" could map to loads of different objects in JVM model, so "x" has no chance of being <immutable>.  "x" just doesn't pin down a concrete object the way ClassNameSym does.

YIKES, what about a template class? Well, presumably class names have to be mangled before they hit the JVM, so we will never see unmangled class names.  But if we do, then ClassNameSym is no longer <immutable> if it is a template class.  The real danger is that some middleman will unmangle the class name, thinking it is doing us a favor.

Because this such a zen subject, reviewed all classes that claim to be <immutable>.  Kicked out ClinitWasCalledSym and GenericMethodNameSym.  So the official <immutable>'s are now

InstanceManagerProxySym
InstructionSym
InvocationSym   (a lot of water under the bridge here)
ClassNameSym
InstructionNameSym
InvocationNameSym
Marker
NullObject
Plug
StringSym
MethodSym
BaseInvariantAgentProxySym

I am worried about StringSym, but leaving it in for now.

Next bug: in ItsAWrap.<init>(), confusion between Object.<init> and Object_MangoFormal.<init>.  You reap what you sow.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/module/definition/msg/AddConjectureTranslateMsg.java
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/Equals.java
    branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateReturnValue.java
    branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteEvent.java
    branches/mango/Mango/Mango/src/mango/worker/engine/sym/ClinitWasCalledSym.java
    branches/mango/Mango/Mango/src/mango/worker/engine/sym/GenericMethodNameSym.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/StackModel.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/model/WorkFlowUtil.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
    branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/a.zip

Added Paths:
-----------
    branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/
    branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/Array length of x is greater than or equal to 10.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/x[5] equals x[6].zip


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