How to apply Hoare Logic to this function

Question

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to get started with using Hoare Logic, I would like to see what it takes for this simple function:

function colorize(integer) {
  var hex = '#'

  if (integer > 1) hex += 'ff'
  else hex += '00'
  if (integer < 100) hex += 'aa'
  else hex += 'bb'
  if (integer > 10) hex += '11'
  else hex += '22'

  return hex
}

My first attempt so far is as follows. I haven't found a resource which describes how to model functions in the Hoare logic, so I just went off the cuff.

\begin{align} \{hex = \# \land integer = y\}\\ if\ (integer > 1)\ hex += ff\\ \{hex = \#ff \land integer = y\}\\ \\ \{hex = \# \land integer = y\}\\ if\ \neg(integer > 1)\ hex += 00\\ \{hex = \#00 \land integer = y\}\\ \\ \{hex = \#\backslash{d}\backslash{d} \land integer = y\}\\ if\ (integer < 100)\ hex += aa\\ \{hex = \#\backslash{d}\backslash{daa} \land integer = y\}\\ \\ \{hex = \#\backslash{d}\backslash{d} \land integer = y\}\\if\ \neg(integer < 100)\ hex += bb\\ \{hex = \#\backslash{d}\backslash{dbb} \land integer = y\}\\ \\ \{hex = \#\backslash{d}\backslash{d} \land integer = y\}\\ if\ (integer > 10)\ hex += 11\\ \{hex = \#\backslash{d}\backslash{d}\backslash{d}\backslash{d11} \land integer = y\}\\ \\ \{hex = \#\backslash{d}\backslash{d} \land integer = y\}\\ if\ \neg(integer > 10)\ hex += 22\\ \{hex = \#\backslash{d}\backslash{d}\backslash{d}\backslash{d22} \land integer = y\}\\ \\ \{hex = \#\backslash{d}\backslash{d}\backslash{d}\backslash{d}\backslash{d}\backslash{d}\}\\ return\ hex\\ \{?\}\\ \\ \{x\}\\ x := colorize(y)\\ \{x = \#\backslash{d}\backslash{d}\backslash{d}\backslash{d}\backslash{d}\backslash{d} \}\\ \\ \{x\}\\ x := length(colorize(y))\\ \{x = 7\} \end{align}

Then the question is, if we need to show explicit examples:

$$\{x\}\ x := colorize(0)\ \{x = \#00aa22\}$$

That wouldn't really make sense because then that's unit testing rather than proving.

Finally, the question is, how to prove that colorize returns the correct outputs.

What I don't understand about Hoare Logic so far is:

1. How to model functions. How to model the "variables are in a certain scope" of the function, as well as calling the function.
2. Which variables to include in the pre- and post-conditions in the example.
3. My understanding is these are Hoare triples (assertions). Are these considered rules or are they different than rules. If they aren't rules, wondering if I need to be creating rules as well somehow. Also not sure what I should be including in the Hoare Triples, if I was too-specific.
4. I saw stuff about partial vs. total correctness. Wondering if I need to somewhere include a proof of termination somehow, or each of these statements.
5. How to write a proof, given these (or the right) Hoare triples.
6. How to handle the "patterns" in the hex string. I just used regular expression digit format $\backslash d$.
7. What counts as a "program" (the middle part of the Hoare Triple). If if (integer > 1) s is one, or does it need to be broken down to the program integer > 1, or is that not a program.

I can follow the explanations of Hoare Triples in introductory presentations, but I am thinking I am a long way from applying it correctly. Looking for help to get over the initial starting complexity, would be helpful to show the specific Hoare Logic statements to define/prove this function, or some of them, so I can build on it.