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 | 3930 reads
|
Browse archives
Active forum topics |
Recent comments
13 weeks 12 hours ago
13 weeks 16 hours ago
13 weeks 16 hours ago
35 weeks 1 day ago
39 weeks 3 days ago
41 weeks 1 day ago
41 weeks 1 day ago
43 weeks 5 days ago
48 weeks 3 days ago
48 weeks 3 days ago