3 ms·
You needn’t think of databases as tables and data, you may think of them as trees of structs, ie an object relational model and show satisfiability of the model
by PartiallyTyped 3y ago
You needn’t think of databases as tables and data, you may think of them as trees of structs, ie an object relational model and show satisfiability of the model by constructing a tree of dependencies.
You can do it incrementally for parts of the model, but that doesn’t guarantee that long range dependencies are satisfiable.
Yes, you then need to show that it is incrementally constructible, which is a different can of worms… the tree view above isn’t actually fully correct because you duplicate entries mapping to the same object. Because of this duplication, the tree may refer to an object that can only be inserted later.
Oh and the encoding must be able to accommodate arbitrary length arrays and arbitrary objects … which makes usage of SMT solvers difficult to say the least.
While I agree that for the average company this isn’t useful, and the average engineer won’t shoot their feet on purpose, what I am doing needs to accommodate all those scenarios because I have no guarantees of sanity.
- auggierose 3y agoNow I am interested in what exactly your use case is :-) Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and proceed from there. But in the end you seem to be looking for a push-button algorithm for proving the consistency of a particular logic, and I can tell you, that's probably not gonna end well.
- PartiallyTyped 3y agoI can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers. If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.