Andrew Haley wrote:
Ian Lance Taylor writes:
> Abramo Bagnara <[EMAIL PROTECTED]> writes:
>
> > I'd like to know if gcc has implemented some generic way to help
> > optimizer job by allowing programmers to specify assumptions (or
> > constraints).
>
> The answer is no, there is nothing quite like you describe.
>
> But I think it would be a good idea.
Something like this would greatly improve the code generation quality
of gcj. There are a great many assertions that I could pass to VRP
and the optimizers: this is invariant, this is less than that, and so
on.
Note that such assertions also can function as predicates to be
discharged in a proof engine. See work on SPARK (www.www.praxis-his.com).
One thing to consider here is whether to implement just a simple
assume as proposed, or a complete mechanism for pre and post
assertions (in particular, allowing you to talk about old values),
then it can serve as
a) a mechanism for programming by contract
b) a mechanism for interacting with proof tools
c) a mechanism to improve generated code as suggested in this thread
all at the same time
Eiffel should be examined for inspiration on such assertions.
Andrew.
