Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: pop3clienthandler.vdmpp Sprache: VDM

Original von: VDM^©

\section{The POP3 Client Handler Class}

\begin{vdm_al}
class POP3ClientHandler

types
\end{vdm_al}

\begin{vdm_al}
types

ServerState = <Authorization> | <Transaction> | <Update>;

\end{vdm_al}

\begin{vdm_al}
values

unknownMessageMsg: seq of char = "No such message";
negativeStatusMsg: seq of char =
                     "Wrong state for this command";
\end{vdm_al}

\begin{vdm_al}
alreadyDeletedMsg: seq of char = "Message already deleted";
deleteFailMsg    : seq of char = "Some deleted messages not removed";
maildropLockedMsg: seq of char = "Maildrop already locked";
maildropReadyMsg : seq of char = "Maildrop locked and ready";
passwordFailedMsg: seq of char = "User/password authentication failed";
quitMsg          : seq of char = "Quitting POP3 Server";
submitPasswordMsg: seq of char = "Enter password";
\end{vdm_al}

\begin{vdm_al}
instance variables
  ss    : ServerState;
  parent: POP3Server;
  user  : POP3Types`UserName;
\end{vdm_al}
\begin{vdm_al}
instance variables
  msgChannel: MessageChannel;
  id: POP3Server`ClientHandlerId;
  lastWasUser: bool := false

\end{vdm_al}

\begin{vdm_al}
operations

public POP3ClientHandler: POP3Server * MessageChannel ==> POP3ClientHandler
POP3ClientHandler(nparent, nch) ==
(
  let - = new IO().echo("Creating POP3ClientHandler") in skip;
  ss := <Authorization>;
  parent := nparent;
  msgChannel := nch
);

\end{vdm_al}

\begin{vdm_al}--[ReceiveCommand]
ReceiveCommand: POP3Types`ClientCommand
                ==> POP3Types`ServerResponse
ReceiveCommand(c) ==
  let response =
    cases c:
      mk_POP3Types`QUIT()    -> ReceiveQUIT(c),
      mk_POP3Types`STAT()    -> ReceiveSTAT(c),
      mk_POP3Types`LIST(-)   -> ReceiveLIST(c),
      mk_POP3Types`RETR(-)   -> ReceiveRETR(c),
      mk_POP3Types`DELE(-)   -> ReceiveDELE(c),
      mk_POP3Types`NOOP()    -> ReceiveNOOP(c),
      mk_POP3Types`RSET()    -> ReceiveRSET(c),
      mk_POP3Types`TOP(-,-)  -> ReceiveTOP(c),
      mk_POP3Types`UIDL(-)   -> ReceiveUIDL(c),
      mk_POP3Types`USER(-)   -> ReceiveUSER(c),
      mk_POP3Types`PASS(-)   -> ReceivePASS(c)
    end
  in
  ( if is_POP3Types`USER(c)
    then lastWasUser := true
    else lastWasUser := false;
    return response
  );

\end{vdm_al}

\begin{vdm_al}
ReceiveQUIT: POP3Types`QUIT ==> POP3Types`ServerResponse
ReceiveQUIT(-) ==
( dcl response: POP3Types`ServerResponse;
  cases ss:
    <Authorization> -> response := mk_POP3Types`OkResponse(quitMsg),
    <Transaction> ->
      let b = parent.RemoveDeletedMessages(user) in
      -- spec is unclear about update state - see pg 10
      -- i.e. quit is actually received in the transaction state and
      -- then the server moves into the update state, but no commands
      -- can be received in the update state
      ( ss := <Update>;
        parent.ReleaseLock(id);
        response := if b
                    then mk_POP3Types`OkResponse(quitMsg)
                    else mk_POP3Types`ErrResponse(deleteFailMsg)
      ),
    others -> error
  end;
  return response
);

\end{vdm_al}

\begin{vdm_al}
ReceiveSTAT: POP3Types`STAT ==> POP3Types`ServerResponse
ReceiveSTAT (-) ==
  if ss = <Transaction>
  then return mk_POP3Types`OkResponse(" " ^
                            int2string(parent.GetNumberOfMessages(user)) ^
                            " " ^
                            int2string(parent.GetMailBoxSize(user)))
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceiveLIST: POP3Types`LIST ==> POP3Types`ServerResponse
ReceiveLIST(list) ==
  if ss = <Transaction>
  then if list.messageNumber = nil or
          parent.IsValidMessageNumber(user, list.messageNumber)
       then let msgs = parent.GetMessageInfo(user, list.messageNumber)
            in
              return mk_POP3Types`OkResponse(MakeScanListHeader(msgs)^"\n"^
                                             MakeScanListing(msgs))
       else return mk_POP3Types`ErrResponse(unknownMessageMsg)
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
functions

MakeScanListHeader: set of POP3Server`MessageInfo -> seq of char
MakeScanListHeader(msgs) ==
  let lp = card msgs in
  int2string(lp) ^ (if lp = 1 then " message(" else " messages(") ^
  int2string(sum({msg.size | msg in set msgs})) ^
  " octets)";

\end{vdm_al}

\begin{vdm_al}
set2seq[@tp]: set of @tp -> seq of @tp
set2seq(s) ==
if s = {}
then []
else let v in set s in
  [v] ^ set2seq[@tp](s \ {v})
measure Size;

Size[@tp]: set of @tp -> nat
Size(list) == card list;

MakeScanListing: set of POP3Server`MessageInfo -> seq of char
MakeScanListing(msgs) ==
  let msgSeq = set2seq[POP3Server`MessageInfo](msgs) in
  MakeMultilineResponse([int2string(msgSeq(i).index) ^ " " ^
                         int2string(msgSeq(i).size)
                        | i in set inds msgSeq]);

\end{vdm_al}

\begin{vdm_al}
MakeMultilineResponse: seq of seq of char -> seq of char
MakeMultilineResponse(resps) ==
  if resps = []
  then []
  elseif len resps = 1
  then hd resps
  else hd resps ^ "\n" ^ MakeMultilineResponse(tl resps)
measure Len;

MakeLineSeq: seq of char -> seq of seq of char
MakeLineSeq(text) ==
  if text = []
  then []
  else let mk_(line, rest) = GetLine(text)
       in
         [line] ^ MakeLineSeq(rest)
measure Len;

GetLine: seq of char -> (seq of char) * (seq of char)
GetLine(text) ==
  if text = []
  then mk_([], [])
  elseif hd text = '\n'
  then mk_([], tl text)
  else let mk_(line, rest) = GetLine(tl text)
       in
         mk_([hd text] ^ line, rest)
measure Len;

Len: seq of char | seq of seq of char -> nat
Len(l) ==
  len l;
\end{vdm_al}

\begin{vdm_al}
sum: set of nat -> nat
sum(s) ==
  if s = {}
  then 0
  else let e in set s in
       sum(s \ {e}) + e
measure Card;

Card: set of nat -> nat
Card(s) ==
  card s;

\end{vdm_al}

\begin{vdm_al}
operations

ReceiveRETR: POP3Types`RETR ==> POP3Types`ServerResponse
ReceiveRETR(retr) ==
  if ss = <Transaction>
  then
    if parent.IsValidMessageNumber(user,
                                   retr.messageNumber)
    then let msgText = parent.GetMessageText(
                                user,
                                retr.messageNumber),
             sizeText =
               int2string(parent.GetMessageSize(
                                   user,
                                   retr.messageNumber))
         in
            return mk_POP3Types`OkResponse(sizeText ^
                                           "\n" ^
                                           msgText)
    else return
           mk_POP3Types`ErrResponse(unknownMessageMsg)
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);
\end{vdm_al}

\begin{vdm_al}
ReceiveDELE: POP3Types`DELE ==> POP3Types`ServerResponse
ReceiveDELE(retr) ==
  if ss = <Transaction>
  then if parent.IsValidMessageNumber(user, retr.messageNumber)
       then ( parent.DeleteMessage(user, retr.messageNumber);
              return mk_POP3Types`OkResponse("message " ^
                                             int2string(retr.messageNumber) ^
                                             " deleted")
            )
       else if parent.MessageIsDeleted(user, retr.messageNumber)
       then return mk_POP3Types`ErrResponse(alreadyDeletedMsg)
       else return mk_POP3Types`ErrResponse(unknownMessageMsg)
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceiveNOOP: POP3Types`NOOP ==> POP3Types`ServerResponse
ReceiveNOOP(-) ==
  if ss = <Transaction>
  then return mk_POP3Types`OkResponse("")
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceiveRSET: POP3Types`RSET ==> POP3Types`ServerResponse
ReceiveRSET(-) ==
  if ss = <Transaction>
  then ( parent.ResetDeletedMessages(user);
         return mk_POP3Types`OkResponse(
                   "maildrop has " ^
                   int2string(parent.GetNumberOfMessages(user))^
                   " messages")
       )
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceiveTOP:  POP3Types`TOP ==> POP3Types`ServerResponse
ReceiveTOP(top) ==
  if ss = <Transaction>
  then if parent.IsValidMessageNumber(user, top.messageNumber)
       then let header = parent.GetMsgHeader(user, top.messageNumber),
                body = parent.GetMsgBody(user, top.messageNumber),
                lines = MakeLineSeq(body)
            in
              return mk_POP3Types`OkResponse(
                        header ^"\n"^
                        MakeMultilineResponse(lines(1,...,
                                              top.numLines)))
       else return mk_POP3Types`ErrResponse(unknownMessageMsg)
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);
\end{vdm_al}

\begin{vdm_al}
ReceiveUIDL: POP3Types`UIDL ==> POP3Types`ServerResponse
ReceiveUIDL(uidl) ==
  if ss = <Transaction>
  then if uidl.messageNumber = nil
       then let uidlTxt = parent.GetAllUidls(user)
            in
              return mk_POP3Types`OkResponse(MakeMultilineResponse(uidlTxt))
       elseif parent.IsMessageNumber(user, uidl.messageNumber)
         -- Note that the spec is unclear here as to whether we should
         -- allow viewing of a specific message's uidl if the message
         -- is marked as deleted
       then return mk_POP3Types`OkResponse(parent.GetUidl(user,
                                                          uidl.messageNumber))
       else return mk_POP3Types`ErrResponse(unknownMessageMsg)
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceiveUSER: POP3Types`USER ==> POP3Types`ServerResponse
ReceiveUSER(usercmd) ==
  if ss = <Authorization>
  then ( user := usercmd.name;
         return mk_POP3Types`OkResponse(submitPasswordMsg)
       )
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);

\end{vdm_al}

\begin{vdm_al}
ReceivePASS: POP3Types`PASS ==> POP3Types`ServerResponse
ReceivePASS(pass) ==
  if ss = <Authorization> and lastWasUser
  then ( lastWasUser := false;
         if parent.AuthenticateUser(user, pass.string)
         then if parent.IsLocked(user)
              then return mk_POP3Types`ErrResponse(maildropLockedMsg)
              else ( parent.AcquireLock(id, user);
                     ss := <Transaction>;
                     return mk_POP3Types`OkResponse(maildropReadyMsg)
                   )
         else return mk_POP3Types`ErrResponse(passwordFailedMsg)
       )
  else return mk_POP3Types`ErrResponse(negativeStatusMsg);
\end{vdm_al}

\begin{vdm_al}
functions

static public int2string: int -> seq of char
int2string(i) ==
  if i = 0
  then "0"
  elseif i < 0
  then "-"^int2string(-i)
  else  int2stringR(i)
measure Abs;

static Abs: int -> nat
Abs(i) ==
  abs i;

static int2stringR: nat -> seq of char
int2stringR(n) ==
  if n = 0
  then ""
  else let first= n div 10,
           last = n mod 10 in
       int2stringR(first) ^
       cases last:
         0 -> "0",
         1 -> "1",
         2 -> "2",
         3 -> "3",
         4 -> "4",
         5 -> "5",
         6 -> "6",
         7 -> "7",
         8 -> "8",
         9 -> "9"
       end
measure Id;

static Id: nat -> nat
Id(n) == n;

\end{vdm_al}

\begin{vdm_al}
thread
( dcl cmd: POP3Types`ClientCommand;
  id := threadid;
  cmd := msgChannel.ServerListen();
  while (cmd <> mk_POP3Types`QUIT()) do
  ( msgChannel.ServerSend(ReceiveCommand(cmd));
    cmd := msgChannel.ServerListen()
  );
  msgChannel.ServerSend(ReceiveCommand(cmd));
)
\end{vdm_al}

\begin{vdm_al}
end POP3ClientHandler
\end{vdm_al}

\begin{rtinfo}
{rtinfo.ast}[POP3ClientHandler]
\end{rtinfo}

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.