Lambda the Ultimate

Seems like there are lots of folks who don't want to go to the trouble of defining contracts or assertions (much) either before or during software development. However, when it comes time to find and fix bugs, there might be more desire to tighten things down.

I've heard of tools that will run your code a zillion times and try to figure out constraints for it (MrFlow is one thing I can think of, but it is apparently more of a static checker). I have not used them so this is a naive question: might such a system work interactively with the developer to construct and refine contracts? Pick a method, and the system starts an interactive Q & A to define and narrow the contract based on the function signiture and any additional information from static analysis, and from having run the code in various ways.

The idea would be to work with the developer / maintainer to over time refine assumptions about the code to find bugs.