\begin{eqnarray*}
  & {} & {\bf function}\ {\tt NNF}\,(\phi )\!:\\
{}& {} & \hbox{/* precondition: \(\phi\) is implication free */}\\
{}& {} & \hbox{/* postcondition: \({\tt NNF}\,(\phi)\) computes a \({\tt NNF}\)
for \(\phi\) */}\\
  & {} & {\bf begin\ function}\\
  & {} & \ \ \ {\bf case}\\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is a literal}\colon \ {\bf return}\
\phi \\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is }\neg\neg \phi _1\colon \ {\bf
return}\
{\tt NNF}\, (\phi_1)\\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is }\phi  _1\land \phi _2\colon \
{\bf return}\ {\tt NNF}\, (\phi  _1)\land {\tt NNF}\, (\phi  _2)\\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is }\phi  _1\lor \phi _2\colon \
{\bf return}\ {\tt NNF}\, (\phi  _1)\lor {\tt NNF}\, (\phi  _2)\\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is }\neg (\phi  _1\land \phi _2)\colon
\
{\bf return}\ {\tt NNF}\, (\neg\phi  _1)\lor {\tt NNF}\, (\neg \phi  _2)\\
  & {} & \ \ \ \ \ \ \phi \ \hbox{is }\neg (\phi  _1\lor \phi _2)\colon
\
{\bf return}\ {\tt NNF}\, (\neg\phi  _1)\land {\tt NNF}\, (\neg \phi  _2)\\
  & {} & \ \ \ {\bf end\ case}\\
  & {} & {\bf end\ function}
\end{eqnarray*}