| Issue 51: | Less conservative joins of existential fractions | |
| 1 person starred this issue and may be notified of changes. | Back to list |
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
Nov 7, 2008
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
Sounds like this is actually done, or at least it is done enough for the current round of case studies.
Status:
Verified
|