On Thu, Feb 26, 2009 at 6:03 PM, Jonathan S. Shapiro <[email protected]> wrote: > Range constraints incur a discharge obligation. In the general case, > this is an unsolved problem in the literature.
Before I forget to say this... There is a meta-level problem with constraints. Success at discharging them is a function of your prover, and nobody seems to have any way to specify what things a prover is *obligated* to prove, nor how to satisfy such an obligation. In consequence, there is no way that a language specification can assure that "integer between 5 and 10" as an obligation can actually be satisfied. This means that in general we lose the ability to specify which programs are valid according to the language definition. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
