next up previous contents
Next: The VDM Operation node Up: VDM Specification of an Previous: The VDM Operation build

The VDM Operations $left\_tree$ and $right\_tree$

The operations left and right are rather more straightforward.


\begin{fn}{left}
\signature{Ordered\_tree \To Ordered\_tree}
\parms{t}
\If t = ...
...n\\ \const{Empty}
\Elseif t = mk-Ord\_bin\_tree(l,val,r)
\Then\\ l \Fi
\end{fn}
Similarly


\begin{fn}{right}
\signature{Ordered\_tree \To Ordered\_tree}
\parms{t}
\If t =...
...n\\ \const{Empty}
\Elseif t = mk-Ord\_bin\_tree(l,val,r)
\Then\\ r \Fi
\end{fn}


Lee McCluskey
2002-12-18