On 1/18/07, Robert Dewar <[EMAIL PROTECTED]> wrote:
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.
Sure. I only was thinking about the interface to the middle-end where new
builtin functions are the easiest way to provide assumptions. If you have
further ideas they are certainly appreciated (without me being required to
research about Eiffel ...).
Thanks,
Richard.
