The slipperiness of optimistic vs pessimistic static analysis

We had a lengthy 
discussion in the context of issue 9 of optimistic vs pessimistic analysis at 
the F2F.  I wanted to show an example that illustrates how slippery even 
the apparently simple definition of optimistic analysis is -- the definition 
being that optimistic analysis rejects only process definitions that are 
*guaranteed* to run into an undefined situation such as uninitialized variable 
use or multiple conflicting receives.  Consider the fragment 
below

 

<scope declares 
variables v1, v2 and v3 ..>

       <invoke inputVariable=v1 
outputVariable=v3 ..>

       use variable v2

</scope>

 

Suppose this 
fragment passes static type checks because v2 and v3 are the same type, and the 
use of v3 in the invoke was a typo -- hit a neighboring key by mistake.  
Should this fail optimistic analysis?  The answer would appear to be yes 
but is actually no according to the definition above because the invoke may 
receive a fault response and hence provide an execution path that does not run 
into the uninitialized variable use problem.  However I believe most 
"reasonable" people would agree that this fragment should be rejected 
regardless.  Even more deviously, a scope may be cancelled by an external 
fault and thus nothing can ever be rejected inside such a scope because the 
scope may be interrupted before reaching the problematic point.  

 

We can try to 
address all such concerns, but in my opinion, any notion that we are going to 
have bug-for-bug portability is not workable.  For instance even thread 
scheduling policies can affect whether an undefined situation happens or 
not.  Thus I would be in favor of not trying to mandate the degree of 
static analysis in every last detail because (A) I think it would be very hard 
to do, and (B) serves little real purpose.

 

Satish