[Date Prev][Date Next][Thread Prev][Thread Next]
[Date Index]
[Thread Index]
**Subject**: **Re: integer exponentiation with negative exponent**
**From**: Coda Highland <chighland@...>
**Date**: Sat, 17 May 2014 08:57:16 -0700

On Sat, May 17, 2014 at 8:48 AM, Thomas Jericke <tjericke@indel.ch> wrote:
> Wait, you're looking at the values of the input now, not the types.
A valid criticism. Doing so adds another tier of complexity to the analyzer.
> Once you analyze that
> you can also analyze x^y for negative values of y.
That's actually a good point.
> Even though I wonder how that sophisticated static analyzer knows the value of 'int'.
It does rather explode the proof tree. When I was doing this for
school I had to put in a LOT of constraints on types and values or
else the prover would go nuts. One time I DID brute-force my way
through a particular theorem without proving enough supplemental
theorems first and it finally resolved, but it generated a 50-page
proof of the theorem in the process. (Having done an offline sketch of
the proof first, I knew it WOULD resolve, and I knew I had sufficient
constraints specified, but I didn't realize just how much of a
combinatoric explosion would be implied by the statement of the
function.)
/s/ Adam