Your axiom is not really an axiom, it's missing hypotheses. Simple presentations of Hoare logic manipulate formulas of the form $\{P\} C \{P'\}$ where $P$ and $P'$ are logical formulas and $C$ is a command. You do need to ensure that $C$ is well-formed. In simple languages such as the ones often used for a first introduction to Hoare logic, well-formedness is syntactic: it's typically a matter of checking that $C$ conforms to a context-free grammar, and possibly that the free variables are within a permitted set. If the language includes constructs that have a semantic correctness, such as accesses to array elements, you need to add hypotheses to express this semantic correctness.
Formally, you can add judgements to express the correction of expressions and commands. If expressions have no side effects, they need no postconditions, only preconditions. For example, you can write well-formedness rules such as
$$
\dfrac{\{P\} \;\; E \text{ wf}}
{\{P \wedge 0 \le E < \mathrm{length}(A)\} \;\; A[E] \text{ wf}}
\qquad
\dfrac{\{P\} \;\; E_1 \text{ wf} \qquad \{P\} \;\; E_2 \text{ wf}}
{\{P\} \;\; E_1 + E_2 \text{ wf}}
$$
and only allow well-formed expressions in commands:
$$
\dfrac{\{P[x\leftarrow E]\} \;\; E \text{ wf}}
{\{P[x\leftarrow E]\} \;\; x := E \{P\}}
$$
A different approach is to treat all expressions as well-formed, but to make any expression involving an ill-formed calculation have a special value $\mathbf{error}$. In languages with run-time bounds checking, $\mathbf{error}$ means “this program raised a fatal exception”. You would then keep track of whether a program errored out through a logical predicate $\mathbf{Error}$; a program is only valid if you can prove that its postcondition implies $\neg\mathbf{Error}$.
$$
\dfrac{}
{\{P[x\leftarrow E]\} \;\; x := E \;\; \{P \vee \mathbf{Error}\}}
\qquad
\dfrac{P[x\leftarrow E] \implies E \not\rightarrow \mathbf{error}}
{\{P[x\leftarrow E]\} \;\; x := E \;\; \{P\}}
$$
Yet another approach is to consider a Hoare triple to hold only if the program terminates correctly. This is the usualy approach for nonterminating programs: the postcondition holds when the command terminates, which might not always happen. If you treat run-time errors as non-termination, you sweep all correctness issues under the hood. You will still need to prove the correctness of the program somehow, but it need not be in Hoare logic if you prefer some other formalism for that task.
By the way, note that expressing what happens when a compound variable such as an array is modified is more involved that what you wrote. Suppose $P$ was, say, $\mathrm{IsSorted}(A)$: the substitution $A[i]\leftarrow E$ would not change $P$, yet the assignment $A[i] \leftarrow P$ might invalidate $P$. Even if you restrict the syntax of predicates to only talk about atoms, consider the assignment $A[A[0]-1] := A[0]$ under the precondition $A[0] = 2 \wedge A[1] = 3$: you cannot make a simple substitution to obtain the correct postcondition $A[0] = 1 \wedge A[1] = 1$, you need to evaluate $A[0]$ (which can be difficult in general, since the precondition might not specify a single possible value for $A[0]$). You need to perform the substitution on the array itself: $A \leftarrow A[i\leftarrow E]$. Mike Gordon's lecture notes have a good presentation Hoare logic with arrays (but without error checking).
