\begin{definition}[Definition:Algorithm/Formal Specification]
An '''algorithm''' can be implemented formally as a computational method $\left({Q, I, \Omega, f}\right)$ as follows:
Let $A$ be a finite set of symbols.
Let $A^*$ be the set of all collations on $A$:
:$\left\{ {x_1 x_2 \cdots x_n: n \ge 0, \forall j: 1 \le j \le n: x_j \in A}\right\}$
The states of the computation are encoded so as to be represented by elements of $A^*$.
Let $N \in \Z_{\ge 0}$.
Let $Q$ be the set of all ordered pairs $\left({\sigma, j}\right)$ where $\sigma \in A^*, j \in \Z: 0 \le j \le N$.
Let $I \subseteq Q$ such that $j = 0$.
Let $\Omega \subseteq Q$ such that $j = N$.
Let $\theta, \sigma \in A^*$.
Then $\theta$ '''occurs in $\sigma$''' {{iff}} $\sigma$ has the form:
:$\alpha \theta \omega$
where $\alpha, \omega \in A^*$.
Let $f$ be a mapping of the following type:
:$f \left({\left({\sigma, j}\right)}\right) = \begin{cases}\left({\sigma, a_j}\right) : & \sigma_j \text { does not occur in } \sigma \\ \left({\alpha \theta_j \omega, b_j}\right) : & \alpha \text { is the shortest element of $A^*$ such that } \sigma  = \alpha \theta_j \omega\end{cases}$
:$f \left({\left({\sigma, N}\right)}\right) = \left({\sigma, N}\right)$
\end{definition}