Re: integer exponentiation with negative exponent

[Coda Highland <chighland@...>]

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