Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: safe_arith.pvs Sprache: VDM

Original von: VDM^©

class POP3Test

values

users : seq of POP3Types`UserName =
  [ "paul",
    "peter",
    "nico",
    "john",
    "marcel"];

passwords : seq of POP3Types`Password =
  [ "laup",
    "retep",
    "ocin",
    "nhoj",
    "lecram"];

headers : seq of seq of char =
  ["From [email protected]\n" ^
   "Subject Subject 1 \n"^
   "Date Fri, 19 Oct 2001 10:52:58 -0500",
   "From [email protected]\n" ^
   "Subject Subject 2 \n"^
   "Date Sat, 20 Oct 2001 10:52:58 -0500",
   "From [email protected]\n" ^
   "Subject Subject 3 \n"^
   "Date Sun, 21 Oct 2001 10:52:58 -0500",
   "From [email protected]\n" ^
   "Subject Subject 4 \n"^
   "Date Mon, 22 Oct 2001 10:52:58 -0500",
   "From [email protected]\n" ^
   "Subject Subject 5 \n"^
   "Date Tues, 23 Oct 2001 10:52:58 -0500"];

bodies : seq of seq of char =
  ["Greetings from Paul",
   "Greetings from Peter",
   "Greetings from Nico",
   "Greetings from John",
   "Greetings from Marcel"];

functions

public MakePasswordMap: () -> map POP3Types`UserName to POP3Types`Password
MakePasswordMap() ==
  { users(i) |-> passwords(i) | i in set inds users };

operations

public MakeMailDrop: () ==> POP3Server`MailDrop
MakeMailDrop() ==
  return
  { users(i) |-> mk_POP3Server`MailBox(MakeMessages(users(i)),
                                       false)
  | i in set inds users};

public MakeMessages: POP3Types`UserName ==> seq of POP3Message
MakeMessages (user) ==
  return
  [ new POP3Message(headers(i),
                    bodies(i) ^ " to " ^ user,
                    user ^ POP3ClientHandler`int2string(i))
  | i in set inds headers ];

functions

TestRun1: () -> seq of POP3Types`ClientCommand
TestRun1() ==
  [ mk_POP3Types`USER(users(1)),
    mk_POP3Types`PASS(passwords(1)),
    mk_POP3Types`STAT(),
    mk_POP3Types`LIST(nil),
    mk_POP3Types`RETR(1),
    mk_POP3Types`DELE(1),
    mk_POP3Types`RETR(1),
    mk_POP3Types`RSET(),
    mk_POP3Types`NOOP(),
    mk_POP3Types`LIST(3),
    mk_POP3Types`LIST(8),
    mk_POP3Types`TOP(2, 5),
    mk_POP3Types`UIDL(nil),
    mk_POP3Types`UIDL(3),
    mk_POP3Types`DELE(1),
    mk_POP3Types`DELE(1),
    mk_POP3Types`UIDL(1),
    mk_POP3Types`QUIT()
  ]

instance variables

   server : POP3Server;
   ch : MessageChannelBuffer;
   mc1 : MessageChannel;
   mc2 : MessageChannel;
   mc3 : MessageChannel;
   send1 : POP3TestSender;
   send2 : POP3TestSender;
   listen1 : POP3TestListener;
   listen2 : POP3TestListener;

operations

public StartServer: POP3Server ==> ()
StartServer(myserver) ==
(  start(myserver);
--   server.WaitForServerStart()
);

public Test1: () ==> ()
Test1() ==
  let ch = new MessageChannelBuffer(),
      server = new POP3Server(MakeMailDrop(), ch, MakePasswordMap())
  in
    ( dcl mc : MessageChannel := new MessageChannel();
      start(server);
      ch.Put(mc);
      let run = TestRun1(),
          send = new POP3TestSender("c", run, mc),
          listen = new POP3TestListener("l", mc)
      in
      ( start(send);
        start(listen);
        listen.IsFinished()
      )
    );

public Test2: () ==> ()
Test2() ==
  let ch = new MessageChannelBuffer(),
      server = new POP3Server(MakeMailDrop(), ch, MakePasswordMap())
  in
    ( dcl mc1 : MessageChannel := new MessageChannel(),
          mc2 : MessageChannel := new MessageChannel();
      start(server);
      ch.Put(mc1);
      ch.Put(mc2);
      let run = TestRun1(),
          send1 = new POP3TestSender("c1", run, mc1),
          send2 = new POP3TestSender("c2", run, mc2),
          listen1 = new POP3TestListener("l1", mc1),
          listen2 = new POP3TestListener("l2", mc2)
      in
      ( start(send1);
        start(send2);
        start(listen1);
        start(listen2);
        listen1.IsFinished();
        listen2.IsFinished();
      )
    );

Start: POP3TestSender | POP3TestListener ==> ()
Start(obj) ==
  start(obj);

public POP3Test:() ==> POP3Test
POP3Test() ==
  (ch := new MessageChannelBuffer();
   server := new POP3Server(MakeMailDrop(), ch, MakePasswordMap());
   mc1 := new MessageChannel();
   mc2 := new MessageChannel();
   mc3 := new MessageChannel();
   send1 := new POP3TestSender("c1", TestRun1(), mc1);
   send2 := new POP3TestSender("c2", TestRun1(), mc2);
   listen1 := new POP3TestListener("l1", mc1);
   listen2 := new POP3TestListener("l2", mc2)
  );

traces

  Two: StartServer(server);
       --let mc in set {mc1,mc2,mc3} in
       (ch.Put(mc1) | ch.Put(mc2) | ch.Put(mc3)){3};
       Start(send1); Start(send2);
       Start(listen1); Start(listen2);
       listen1.IsFinished();
       listen2.IsFinished();

end POP3Test

class POP3TestSender

instance variables

id   : seq of char;
cmds : seq of POP3Types`ClientCommand;
mc   : MessageChannel

operations

public POP3TestSender: seq of char * seq of POP3Types`ClientCommand *
                       MessageChannel ==> POP3TestSender
POP3TestSender(idarg, cmdsarg, mcarg) ==
( id := idarg;
  cmds := cmdsarg;
  mc := mcarg
);

LogClient: POP3Types`ClientCommand ==> ()
LogClient(cmd) ==
  let io = new IO() ,
      - = io.echo("Client " ^ id ^ " says -> "),
      - = io.writeval[POP3Types`ClientCommand](cmd)
  in
    skip;

SendCmd: MessageChannel * POP3Types`ClientCommand ==> ()
SendCmd(mcarg, cmd) ==
( mcarg.ClientSend(cmd);
  LogClient(cmd);
);

thread
  for cmd in cmds do
    SendCmd(mc, cmd);

end POP3TestSender

class POP3TestListener

instance variables

id : seq of char;
mc : MessageChannel;
finished : bool

operations

public POP3TestListener: seq of char * MessageChannel ==> POP3TestListener
POP3TestListener(idarg, mcarg) ==
( id := idarg;
  mc := mcarg;
  finished := false;
);

LogServer: POP3Types`ServerResponse ==> ()
LogServer(resp) ==
  let io = new IO() ,
      - = io.echo("Server " ^ id ^ " responds -> "),
      - = io.writeval[POP3Types`ServerResponse](resp)
  in
    skip;

public IsFinished: () ==> ()
IsFinished() ==
  skip;

sync
  per IsFinished => finished

thread
( dcl response : POP3Types`ServerResponse := mc.ClientListen();
  while response <> mk_POP3Types`OkResponse( "Quitting POP3 Server" )
  do
  ( LogServer(response);
    response := mc.ClientListen()
  );
  LogServer(response);
  finished := true
)

end POP3TestListener

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.