Basically the title, I'm not sure which one is formal:
$$ \begin{aligned} division:\mathbb{R} \times \mathbb{R} &\rightarrow \mathbb{R} \cup \text{\{"impossible"\}} \\ (x,y) &\mapsto \begin{cases} x/y, & \text{if $y \neq 0$} \\ \text{"impossible''}, & \text{else} \end{cases} \end{aligned} $$
Or
$$ \begin{aligned} division:\mathbb{R} \times \mathbb{R}\backslash\{0\} &\rightarrow \mathbb{R} \\ (x,y) &\mapsto x/y \end{aligned} $$
You can exclude denominators equal to zero right from the start: $$\begin{align} \operatorname{div}:\Bbb R \times \Bbb R_{\neq0}&\to\Bbb R \\ (x,y) &\mapsto x / y \end{align}$$
So you know that arguments of the form $(x,0)$ are not valid, just like you already know that arguments like $(x,\mathrm{flowerpot})$ are not valid because "flowerpot" is not a valid denominator as it's not an element of $\Bbb R\!\setminus\!\{0\}$.
Well, in a purely mathematical context, I'd chose the second.
But you mentioned in your comment that this function is intended to be implemented in a computer program, presumably using IEEE 754 floating-point representation, so here's a slightly more apt version for that context.
Let $\mathbb{R}' = \mathbb{R} \cup \lbrace +\infty, -\infty, \text{NaN}, -0 \rbrace$. This an extended real number line including the IEEE 754 special values. Then:
$$\text{division}: \mathbb{R}' \times \mathbb{R}' \mapsto \mathbb{R}' \\ (x, y) \mapsto \begin{cases} x/y & \text{if } x \in \mathbb{R} \text{ and } y \in \mathbb{R}\backslash \lbrace 0 \rbrace \\ 0 & \text{if } x \in \mathbb{R} \text{ and } y \in \lbrace +\infty, -\infty \rbrace \\ +\infty & \text{if } (x > 0 \text{ and } y = +0) \text { or } (x < 0 \text{ and } y = -0) \\ +\infty & \text{if } (x = +\infty \text { and } y > 0) \text{ or } (x = -\infty \text { and } y < 0)\\ -\infty & \text{if } (x < 0 \text{ and } y = +0) \text { or } (x > 0 \text{ and } y = -0) \\ -\infty & \text{if } (x = -\infty \text { and } y > 0) \text{ or } (x = +\infty \text { and } y < 0)\\ \text{NaN} & \text{otherwise} \end{cases} $$
I'm probably way overthinking this, though.
If you want to formalize a division operation that returns a sentinel value $null$ for "no output", then you should also expand the domain of the function representing that operation to $R'=ℝ∪\{null\}$ and define $div : R'×R'→R'$ via:
$(x,y) = x/y$ for each $x∈ℝ$ and $y∈ℝ∖\{0\}$.
$(x,y) = null$ for each $x∈ℝ$ and $y = 0$.
$(x,y) = null$ for each $x,y∈R'$ such that $x = null$ or $y = null$.
The first part captures the standard division. The second captures "no answer for division by zero". The third is the usual null-propagation (i.e. if an input is missing then the output is missing too).
Beware that there are tons of different meanings for "$null$" and this is just one common one that is incompatible with the meaning of null in object-oriented programming languages that support comparison between null pointers. In contrast, any semantics that has null-propagation should also stipulate that "$null=null$" evaluates to $null$. For instance, "$1/0 = 0/0$" evaluates to $null$ as desirable.
Note that the meaning of $null$ used here is compatible with the formalization of partial functions as standard functions that may map an input to $null$, and composition of these maybe-$null$ functions exactly match the composition of the original partial functions. But many logicians do not like this extra $null$ possibility, and it's usually mathematically cleaner to stick to standard functions.
