| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/POP3PP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 11 kB |
|
Quelle pop3clienthandler.vdmpp Sprache: 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.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28