SSL pop3clienthandler.vdmpp  Sprache: unbekannt

\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}