How can I formalize key value stores with set theory?

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I found article about key value formalisation with category theory, but I'm interested are there some works about formalisation of key-value stores except category theory (I know we can use it for all, but...)? I want to use some more simple and lightweight mathematics for mathematical description of key-value stores. And I feel that set theory will be enough for this, but couldn't find any helpful articles.

• What have you tried so far? What specifically are you stuck on? It's hard to know how to help you without seeing how far you've got and what level of answer or detail you're looking for. – D.W. Apr 22 '15 at 18:33
• Cross-posted on CSTheory: cstheory.stackexchange.com/q/31214/5038. For the future, please don't cross-post, as it is forbidden by our site rules and it is impolite to answerers (as it fragments answers and discussions). – D.W. Apr 23 '15 at 22:06

One simple way to model a key-value store is as a map $f:K \to V$ where $K$ is the set of possible keys and $V$ is the set of possible values.
Often, each value $v \in V$ will itself be a tuple or record. You can represent a tuple as a Cartesian cross-product, e.g., $V = V_1 \times V_2 \times \dots \times V_k$. You can represent a record as either a tuple (if the set of attributes is finite and known in advance), or as a function from attribute names to values.
Modelling languages like Alloy can represent such maps natively. Some modeling languages will use the notation $k.f$ instead of $f(k)$ (i.e., object field access notation instead of function evaluation), but the two are equivalent.
If you don't want to use functions, but want to stick to just sets, that is also feasible. You can model any function $f: K \to V$ as a binary relation, i.e., a set $S \subseteq K \times V$ with the additional property that if $(k_1,v_1) \in S$ and $(k_2,v_2) \in S$ and $k_1=k_2$, then $v_1=v_2$. However this may be less natural.