How to apply Operational Semantics to this function
You are looking for Hoare logic. Writing out the answer to the question would pretty much amount to copying the introduction to Hoare logic from Wikipedia. I suggest that you have a look at proving program correctness using Hoare logic, and try to apply it to your problem. It's actually an easy case because there are no loops. If you get stuck, come back and ask a specific question about Hoare logic.

I would break up the problem into proving several properties about hex:


The length of hex is 7 at the end.
The first character of hex is #.
All characters, except the first one, are hexadecimal digits.


Also not that the proof does not require you to write out any operational semantics. You can just use the Hoare logic to argue about your program, and there is a theorem which guarantees that Hoare logic is correct with respect to the standard operational semantics.