|
\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)
¤
|
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.
|
