My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
  Advanced search   Search tips   Subscriptions
Issue 51: Less conservative joins of existential fractions
1 person starred this issue and may be notified of changes. Back to list
Status:  Verified
Owner:  kevin.bi...@gmail.com
Closed:  Jul 2009


 
Project Member Reported by kevin.bi...@gmail.com, Nov 4, 2008
When joining permissions with different existential fractions we currently
generate a new existential fraction.  This fails to work with correlated
implications, which cannot be applied any more, and also increases the
overhead because joins are needed at all subsequent nodes in, say, a loop
body as well.  

It should be possible to alpha-convert existential fractions and reduce the
need for fresh existential fractions, but without compromising correct
reasoning about universally quantified fractions coming from a
method-precondition.
Nov 4, 2008
Project Member #1 kevin.bi...@gmail.com
r150 attempts to track universally quantified fractions
Nov 7, 2008
Project Member #2 kevin.bi...@gmail.com
r153 implements join based on recognized alpha-convertable existentials.  

Thinking it might be better to just remember in NamedVariable whether it's a
universal or existential, instead of in FractionConstraints.
Jul 23, 2009
Project Member #3 nels.bec...@gmail.com
Sounds like this is actually done, or at least it is done enough for the current round 
of case studies.
Status: Verified

Powered by Google Project Hosting