3 ms·

Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is act

Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is actually any such database, or if the property is always false. Second, assuming that there are any such databases: Given certain commands which operate on databases, is there any sequence of commands which transform the empty database into a database such that the schema property holds for it? Actually, you probably would want the property to be true for every intermediate step as well, right? Sounds interesting! Although in practice, solving this is probably not that important, because if you cannot come up with some examples of constructing databases for your schema and application, then the schema is the wrong one pretty much by definition.

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 ago
  Now 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 ago
    I 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.

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 ago
Now 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 ago
  I 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.