User loginNavigation |
Specifying Solver Behavior?In a recent discussion about adding some dependent typing capabilities in BitC, it was proposed that we should instead statically reject programs that contain unsolved constraints, and require that the programmer take responsibility for inserting checks explicitly. The idea is that these checks can still be compiled out, but making them visible to the developer may have the effect of diagnosing bugs or inducing better arrangements of code. I'm not yet fully convinced, but I'm thinking about it. Here is the "catch" that I see: When unsolved constraints lead to compile-time program rejection, the behavior of the solver becomes part of the language specification. It becomes necessary to specify a standard set of verification conditions that the compiler must generate (which seems straightforward), a standard rule base over which the solver must operate, and a standard behavior by which the solver must combine these rules. Individual implementations are certainly free to use better solvers, rule bases, or verification conditions but the language specification must define precisely what constitutes a "compliant" program, and compilers must retain the capability to identify programs that are not transportable (that is: programs that would not be accepted if the enhanced solver were not applied). Finally, if the language definition is to be deterministic, it would seem to follow that the reference solver must operate by exhaustive search, and must be assured to terminate. So two questions:
Anyway, what is the state of the art concerning solver specification? By shap at 2009-01-11 19:02 | LtU Forum | previous forum topic | next forum topic | other blogs | 3964 reads
|
Browse archives
Active forum topics |
Recent comments
22 weeks 6 days ago
22 weeks 6 days ago
22 weeks 6 days ago
45 weeks 19 hours ago
49 weeks 2 days ago
50 weeks 6 days ago
50 weeks 6 days ago
1 year 1 week ago
1 year 6 weeks ago
1 year 6 weeks ago