Quelle messagechannel.vdmpp Sprache: VDM

\section{The Message Channel Class}

\begin{vdm_al}
class MessageChannel

instance variables
\end{vdm_al}

\begin{vdm_al}
instance variables
  data : [POP3Types`ClientCommand |
          POP3Types`ServerResponse]  := nil;
\end{vdm_al}

\begin{vdm_al}
instance variables

io : IO := new IO();
debug : bool := true;
\end{vdm_al}

\begin{vdm_al}
operations

Send: POP3Types`ClientCommand |
      POP3Types`ServerResponse ==> ()
Send(msg) ==
  data := msg;

Listen: () ==> POP3Types`ClientCommand |
               POP3Types`ServerResponse
Listen() ==
let d = data in
  ( data := nil; return d
  );
\end{vdm_al}

\begin{vdm_al}
operations

public ServerSend: POP3Types`ServerResponse ==> ()
ServerSend(p) ==
( if debug
  then let - = io.echo("***> ServerSend")
       in skip;
  Send(p);
  if debug
  then let - = io.echo("***> fin ServerSend")
       in skip
);
\end{vdm_al}

\begin{vdm_al}
public ClientListen: () ==> POP3Types`ServerResponse
ClientListen() ==
( if debug
  then let - = io.echo("***> ClientListen")
       in skip;
  let r = Listen(),
      - = if debug
          then io.echo("***> fin ClientListen")
          else false
  in
    return r;
);

public ClientSend: POP3Types`ClientCommand ==> ()
ClientSend(p) ==
( if debug
  then let - = io.echo("***> ClientSend")
       in skip;
  Send(p);
  if debug
  then let - = io.echo("***> fin ClientSend")
       in skip;
);

public ServerListen: () ==> POP3Types`ClientCommand
ServerListen() ==
( if debug
  then let - = io.echo("***> ServerListen")
       in skip;
  let c = Listen(),
      - = if debug
          then io.echo("***> fin ServerListen")
          else false
  in
    return c
);
\end{vdm_al}

\begin{vdm_al}
sync
  per ServerListen => #fin(ClientSend) - 1 =
                      #fin(ServerListen);
\end{vdm_al}

\begin{vdm_al}
  per ClientListen => #fin(ServerSend) - 1 = #fin(ClientListen);
\end{vdm_al}

\begin{vdm_al}
  per ServerSend => #fin(ClientSend) = #fin(ServerListen) and
                    #fin(ServerListen) - 1 = #fin(ServerSend);
\end{vdm_al}

\begin{vdm_al}
  per ClientSend => #fin(ServerSend) = #fin(ClientListen)
                    and
                    #fin(ClientSend) = #fin(ServerListen)
                    and
                    #fin(ServerSend) = #fin(ClientSend) ;

end MessageChannel
\end{vdm_al}

quality89%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.