Set of ordered pairs notation

Question

I am working on my bachelor's thesis, and I have problem formally specifying constraints on one of the components.

Bachelor's thesis is in the field of Computer Science, and I am expressing one of the components of system I designed as set of ordered pairs ${(name,value),...} $(implemented as hashmap name -> value). I need to define constraint of this component, so that each $name$ is unique - no 2 elements share same $name$. So far I have come up with this: $\forall(n1,v2) \in Values, \nexists(n2,v2) \in Values: n1==n2 $

Also, I am writing several algorithms describing real implementation, and for this purpose I would like to use map notation $arr[n] = v; v = arr[n]$. I have defined it as so:

Let $arr$ be set containing elements, where each element is an ordered pair $(n,v)$. Notation $arr[n] = v$ denotes insertion operation into this set so the resulting set will be $arr = arr ∪ {(n,v)}$. Notation $v = arr[n]$ denotes selection and projection operation $((a,v) ∈ arr ∧ a == n) → v$.

My background in mathematics is pretty slim, but I would like to express these details as formally, and clearly as possible.

Answer 1

For the first part, your example is bad because you didn't specify that $v_1\neq v_2$. In other words, the set $\{(a,b)\}$ does not satisfy your condition because I can set $n_1=n_2=a$ and $v_1=v_2=b$.

---

I would say the easiest way would be to say $$\forall n\in\text{Names},\forall v_1, v_2\in\text{Names}:(n, v_1)\in\text{Values}\land(n, v_2)\in\text{Values}\implies v_1=v_2$$

---

For the second part, the operation $arr=arr\cup (n, v)$ does not say what happens when $(n, v')$ is already in $arr$.