\section*{Appendix: ObjectSisal Specifications}
\label{appendix}

In this appendix we give ObjectSisal programs that are
executable specifications of the three object modules of the
illustrative telephone exchange. The top-level specification
has already been given as the {\tt Exchange} class in
Figure~\ref{exchange-class}. The program for each component module
is a class
definition that includes a tail-recursive {\tt Process} operation
that acts on successive elements (events) of an input stream. In each
case, the {\tt Process} operation may be regarded as a state machine;
it is a trivial state machine (one state) in the cases of the
CCU and the SWU, where the action taken is determined by the
next input event and is selected by a simple {\tt case}
expression. In the case of the PLU a two-level {\tt case} expression
is used because the action taken is determined by the combination of phone
line state and input event. We have extended Sisal here by
allowing the tags of a nested union type to be combined by a
dot, thereby avoiding a nested case expression.
Each class has a {\tt Create} operation for use in
creating an instance (object) of its principal type. 

The common control unit is specified by the {\tt CCU} class in
Figure~\ref{ccu}. Its {\tt ProcessStep} operation
(Figures~\ref{ccu-step1} and~\ref{ccu-step2}) generates the streams
of command events sent to the SWU and the response signals to the PLUs.
A special private function {\tt EnterLineEvent}
(Figure~\ref{enter-line}) is used to construct an array of prefix streams
(most of them empty) containing any output events to be sent to PLUs. It
serves as a {\em distributor} of output events to
the various PLUs.
It is a pure function, as are all operations of the three classes
defined here, with the exception of the {\tt Process} operation of
the {\tt PLU} class which combines input streams using the
nondeterminate merge operator.

\begin{figure}\small\center
\begin{verbatim}
class CCU is

  line_cnt: integer;

  function Create (n: integer returns CCU )

    object CCU [line_cnt: n]

  end function Create;

  function Process (
    in_stream: stream of InEvent;
    returns
      array of stream of LineOutEvent,
      stream of SwitchOutEvent )
  
    let origin := array_fill (1, line_cnt, 0);
    in
      ProcessStep ( origin, in_stream )
    end let
  end function Process

  private function ProcessStep (
    origin: array of Number;
    in_stream: stream of InEvent;
    returns
      array of stream of LineOutEvent,
      stream of SwitchOutEvent )

    ------
    ------

  private function EnterLineEvent
  
    ------
    ------

end class CCU
\end{verbatim}
\caption{\label{ccu} The class {\tt CCU}, specifying the common
   control unit.}
\end{figure}


\begin{figure}\small\center
\begin{verbatim}
  private function ProcessStep (
    origin: array of Number;
    in_stream: stream of InEvent;
    returns
      array of stream of LineOutEvent,
      stream of SwitchOutEvent )
    let
      in_tail := stream_rest (in_stream);
      in_event := stream_first (in_stream);
      new_origin, plu_events, swu_events :=
        case in_event of
          line:
            let
              line := in_event.tag;
              event := in_event.event;
            in case event of
                seize:
                  origin,
                  stream [],
                  stream [union SwitchOutEvent [
                    connect: record [
                      calling: line;
                      called: event.called ] ];
                answer:
                  let
                    calling_line := origin [line];
                    line_event := union LineOutEvent [
                      command.stop_ring ];
                  in
                    origin,
                    EnterLineEvent (plu_events, calling_line, line_event),
                    stream [union SwitchOutEvent [
                      connect: record [
                        calling: line;
                        called: event.called ] ]
                  end let;
                clear:
                  origin [line: 0],
                  stream [],
                  stream [union SwitchOutEvent [
                    disconnect: record [line: line] ];
              end case
            end let;
\end{verbatim}
\caption{\label{ccu-step1}Specification of the
   Common Control Unit. Part 1: Line events.}
\end{figure}



\begin{figure}\small\center
\begin{verbatim}
          switch.success:
            let
              calling_line := in_event.calling;
              called_line := in_event.called;
              line_event_a := union LineOutEvent 
                [command.ring_tone];
              line_event_b := union LineOutEvent 
                [command.ring];
            in
              origin [called_line: calling_line],
              EnterLineEvent (
                EnterLineEvent (
                  plu_events, calling_line, line_event_a),
                  called_line, line_event_b),
              stream []
            end let;
          switch.fail:
            let
              calling_line := in_event.calling;
              line_event_a := union LineOutEvent [
                command.busy_tone];
            in
              origin,
              EnterLineEvent (plu_tail, A, line_event_a),
              stream []
            end let;
        end case
      plu_tail, swu_tail := Process (new_origin, in_tail);
      plu_out_streams :=
        for line in 1..line_cnt do
          plu_out_stream := plu_events [line] || plu_tail [line];
        returns array of plu_out_stream
        end for
      swu_out_stream := swu_events || swu_tail;
    in
      plu_out_streams,
      swu_out_stream
    end let
  end function ProcessStep
\end{verbatim}
\caption{\label{ccu-step2}Specification of the
   Common Control Unit. Part 2: Switch events.}
\end{figure}

\begin{figure}\small\center
\begin{verbatim}
  private function EnterLineEvent (
      plu_events: array of stream of LineOutEvent;
      line: Number;
      event: LineOutEvent;
      returns array of stream of LineOutEvent )
    for i in [1..line_cnt] do
      line_events :=
        if i = line
        then stream [ event ] || plu_events [i]
        else plu_events [i]
        end if;
    returns array of line_events
    end for;
  end function EnterLineEvent
\end{verbatim}
\caption{\label{enter-line}The auxiliary function {\tt
   EnterLineEvent} for the {\tt CCU} class.}
\end{figure}

The phone line unit is specified by the {\tt PLU} class
shown in Figure~\ref{line-class}. As in the {\tt Exchange} class, 
the two input streams are merged and presented to the
{\tt ProcessStep} function with the initial state {\tt Idle}.
The coding of the {\tt ProcessStep} function
(Figures~\ref{line-step1} and~\ref{line-step2})
is straightforward. The specification of the switch unit,
given in Figure~\ref{switch-unit},
involves no new features. However, we have not indicated a
representation for the SWU state, but use the unelaborated
functions {\tt FreePath}, {\tt AddPath}, and {\tt DeletePath}
to test and modify connections made through the switch.

\begin{figure}\small\center
\begin{verbatim}
class PLU is

  type LineEvent = union [
    external: LineExtEvent;
    command: LineOutEvent ];

  type LineState = union [
    Idle, Dialing, Connect, RingTone, BusyTone, Ring, Speech];

  function Create ( returns PLU )
    object PLU
  end function Create;

  function Process (
    Ex: stream of LineExtEvent;
    Eo: stream of LineOutEvent;
    returns
        stream of PhoneState,
        stream of LineInEvent )
    let
      El := merge ( Ex, Eo );
      S0 := union LineState [Idle]; 
    in  ProcessStep (El, S0)
    end let
  end function Process;

  private function ProcessStep
      ------
      ------
  end function ProcessStep

end class PLU
\end{verbatim}
\caption{\label{line-class} The class {\tt PLU}, specifying
   the phone line unit.}
\end{figure}


\begin{figure}\small\center
\begin{verbatim}
private function ProcessStep (
    in_stream: stream of LineEvent;
    S:  LineUnitState;
    returns
        stream of LineInEvent,
        stream of PhoneState )
  let
    in_event := stream_first ( in_stream );
    in_tail := stream_rest ( in_stream );
    out_flag, out_event, status, new_state :=
      case S of
        Idle: case in_event of
            external.off_hook:
              false, record [],
              union PhoneState [dialing],
              union LineState [Dialing];
            command.ring:
              false, record [],
              union PhoneState [ring],
              union LineState [Ring];
            otherwise:
              false, record [],
              union PhoneState [idle] ),
              union LineState [Idle] );
          end case
        Dialing: case in_event of
            external.on_hook:
              false, record [],
              union PhoneState [idle],
              union LineState [Idle];
            external.digits:
              let
                dialed := digits;
              in true,
                union LineInEvent [seize: record [
                  called: dialed] ],
                union PhoneState [connect],
                union LineState [Connect]   
              end let;
            otherwise: false, record [],
              union PhoneState [dialing]
              union LineState [Dialing];
          end case
\end{verbatim}
\caption{\label{line-step1}State transition function of the
    phone line unit. Part 1.}
\end{figure}


\begin{figure}\small\center
\begin{verbatim}
        Ring: case in_event of
            external.off_hook: true,
              union LineInEvent [answer],
              union PhoneState [speech],
              union LineState [Speech];
            otherwise: false, record [],
               union PhoneState [ring];
               union LineState [Ring];
          end case 
        Connect: case in_event of
            external.on_hook: true,
              union LineInEvent [clear],
              union PhoneState [idle],
              union LineState [Idle];
            command.ring_tone: false, record [],
              union PhoneState [ring_tone],
              union LineState [RingTone];
            command.busy_tone: false, record [],
              union PhoneState [busy_tone],
              union LineState [Busy];
            otherwise: false, record [],
              union PhoneState [connect],
              union LineState [Connect];
          end case 
\end{verbatim}
\caption{\label{line-step2}State transition function of the
    phone line unit. Part 2.}
\end{figure}


\begin{figure}\small\center
\begin{verbatim}
        RingTone: case in_event of
            external.on_hook: true,
              union LineInEvent [ clear: record [calling: self]],
              union PhoneState [idle],
              union LineState [Idle];
            command.stop_ring: false, record [],
              union PhoneState [speech],
              union LineState [Speech];
            otherwise:
              false, record [],
              union PhoneState [ring_tone],
              union LineState [RingTone];
          end case 
        Busy: case in_event of
            external.on_hook: true,
              union LineInEvent [ clear: record [calling: self] ],
              union PhoneState [idle],
              union LineState [Idle];
            otherwise: false, record [],
              union LineUnitState [busy];
          end case 
        Speech: case in_event of
            external.on_hook: true,
              union LineInEvent [clear: record [calling: self] ],
              union PhoneState [idle],
              union LineState [Idle];
            otherwise: false, record [],
              union PhoneState [speech],
              union LineState [Speech];
          end case 
      end case

      out_tail, status_tail := Process ( in_tail, new_state );
    in if out_flag then
        stream [out_event] || out_tail,
        stream [status] || status_tail,
      else
        out_tail,
        stream [status] || status_tail,
      end if
    end let

  end function ProcessStep
\end{verbatim}
\caption{\label{line-step3}Transition function for the
   phone line unit. Part 3.}
\end{figure}


\begin{figure}\small\center
\begin{verbatim}
class SWU is

  type SwitchState = ... ;

  function Create (state0: State;
    returns SWU )
    object SWU [];
  end function Create;

  function Process (
      in_stream: stream of SwitchOutEvent;
      returns stream of SwitchInEvent )
    ProcessStep (in_stream, switch_initial_state);
  end function Process;

  prviate function ProcessStep (
    in_stream: stream of SwitchOutEvent; 
    state: SwitchState
    returns stream of SwitchInEvent )
    let
      in_event := stream_first (in_stream);
      in_tail := stream_rest (in_stream);
      switch_events, new_state :=
       case event of
         seize: if FreePath ( state, in_event.calling, in_event.called ) 
           then
             stream [ union SwitchInEvent [ success: record [
               calling: in_event.calling;
               called: in_event.called ] ] ],
             AddPath ( state, in_event.calling, in_event.called )
           else stream [ union SwitchInEvent [ fail: record [
               calling: in_event.calling ] ] ],
             state
           end if
         clear: stream [], 
           DeletePath ( state, in_event.line );
       end case
    in
      switch_events || ProcessStep (in_tail, new_state)
    end let
  end function ProcessStep
end class SWU
\end{verbatim}
\caption{\label{switch-unit}Executable specification of the
   switch unit.}
\end{figure}

\begin{figure}\small\center
\begin{verbatim}
  private function TagStream (
    line: integer;
    strm: stream of LineEvent;
    returns stream of TaggedLine Event )
    
    stream [ record [
        tag: line;
        event: stream_first (strm) ] ||
      TagStream (line, stream_rest (strm)
  end function TagStream
\end{verbatim}
\caption{\label{tag-sisal}The {\tt TagStream} function
   for tagging phone line events with the line number.}
\end{figure}

For completeness we also give (Figure~\ref{tag-sisal}) the coding
of the {\tt TagStream} function
used in the {\tt Run} operation of the {\tt Exchange} class.



