Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/POP3PP/   (Wiener Entwicklungsmethode ©)  Datei vom 13.4.2020 mit Größe 6 kB image not shown  

Quelle  pop3test.vdmpp   Sprache: 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 paul@mail.domain\n" ^
   "Subject Subject 1 \n"^
   "Date Fri, 19 Oct 2001 10:52:58 -0500",
   "From peter@mail.domain\n" ^
   "Subject Subject 2 \n"^
   "Date Sat, 20 Oct 2001 10:52:58 -0500",
   "From nico@mail.domain\n" ^
   "Subject Subject 3 \n"^
   "Date Sun, 21 Oct 2001 10:52:58 -0500",
   "From john@mail.domain\n" ^
   "Subject Subject 4 \n"^
   "Date Mon, 22 Oct 2001 10:52:58 -0500",
   "From marcel@mail.domain\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

93%


¤ Dauer der Verarbeitung: 0.12 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.