|
\section{The System Class}
The System class is collecting all the different parts of the system together.
\begin{vdm_al}
class System
values
c1 : Card = new Card(123456,1,1);
c2 : Card = new Card(123457,2,2);
c3 : Card = new Card(123458,3,3);
c4 : Card = new Card(123459,4,4);
c5 : Card = new Card(123460,5,5);
c6 : Card = new Card(123461,6,5);
c7 : Card = new Card(123462,7,5);
cards : set of Card = {c1,c2,c3,c4,c5,c6,c7};
resource : CentralResource = new CentralResource();
tills : map TillId to Till =
{1 |-> new Till(resource),
2 |-> new Till(resource),
3 |-> new Till(resource)};
instance variables
clock : Clock := new Clock();
letterbox : Letterbox := new Letterbox();
types
public TillId = nat;
operations
public GetTill: TillId ==> Till
GetTill(tid) ==
return tills(tid);
public GetResource: () ==> CentralResource
GetResource() ==
return resource;
public System: () ==> System
System() ==
(clock.SetDate("150999");
let peter = new Cardholder().Create("Peter Gorm Larsen",
"Granvej 24"),
paul = new Cardholder().Create("Paul Mukherjee",
"Rugaardsvej 47"),
sten = new Cardholder().Create("Sten Agerholm",
"Teisensvej ??"),
kim = new Cardholder().Create("Kim Sunesen",
"??"),
CSK = new Cardholder().Create("CSK","Forskerparken 10A")
in
let pglacc1 = new Account().Create({1 |-> peter},5000),
saacc1 = new Account().Create({2 |-> sten},0),
ksacc1 = new Account().Create({3 |-> kim},9000),
pmacc1 = new Account().Create({4 |-> paul},6000),
ifacc1 = new Account().Create({5 |-> peter,
6 |-> sten,
7 |-> CSK},70000),
pglid1 = 1,
said1 = 2,
ksid1 = 3,
pmid1 = 4,
ifid1 = 5
in
(resource.AddAccount(pglid1,pglacc1);
resource.AddAccount(said1,saacc1);
resource.AddAccount(ksid1,ksacc1);
resource.AddAccount(pmid1,pmacc1);
resource.AddAccount(ifid1,ifacc1);
-- tills := ;
-- cards := {c1,c2,c3,c4,c5,c6,c7};
resource.AddLetterbox(clock,new Letterbox())));
traces
T1: let c in set cards
in
let t in set rng tills
in
let p in set {123456,123457,123458,123459,123460,123461,123462}
in
(t.InsertCard(c);t.Validate(p);t.MakeWithdrawal(1000))
T2: let c in set cards
in
let t1, t2 in set rng tills
in
let p in set {123456,123457,123458,123459,123460,123461,123462}
in
((t1.InsertCard(c);
t2.InsertCard(c);
t1.Validate(p);
t1.MakeWithdrawal(1000);
t2.MakeWithdrawal(1000))|
(t1.Validate(p);
t1.MakeWithdrawal(3000)) )
end System
\end{vdm_al}
¤ 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.
|
