Hello all,
Actually, a prototype for declaring and proving properties in Clean has been
implemented and will be upgraded to a fully integrated language tool. Simple
properties about higher-order functions can be declared in a Clean-program
and then proven by/with the prover. Properties that can be proven
automatically are for example:
x + y = y + x for all x,y
sum (map (+1) x) = (sum x) + (length x) for all x
It is then up to the compiler to actually use these properties to generate
better code.
The prototype and a paper describing it (submitted for IFL'98) can be found
on http://www.cs.kun.nl/~maartenm
Maarten de Mol
