|
state System of
accounts : map AccountId to Account
illegalCards : set of CardId
curCard : [Card]
cardOk : bool
retainedCards : set of Card
inv mk_System(accs,-,curCard,cardOk,-) ==
(curCard = nil => not cardOk) and
(forall id1, id2 in set dom accs &
id1 <> id2 =>
dom accs(id1).cards inter dom accs(id2).cards = {})
init s == s = mk_System({|->},{},nil,false,{})
end
types
Account :: cards : map CardId to Cardholder
balance : nat
transactions : seq of Transaction
inv account == TransactionsInvariant(account.transactions);
Transaction :: date : Date
cardId : CardId
amount : nat;
Card :: code : Code
cardId : CardId
accountId : AccountId;
Cardholder :: name : Name;
AccountId = nat;
Name = seq of char;
CardId = nat;
Code = nat;
PinCode = nat;
Date = seq of char;
functions
TransactionsInvariant : seq of Transaction +> bool
TransactionsInvariant(ts) ==
forall date in set {t.date | t in seq ts} &
DateTotal(date,ts) <= dailyLimit;
DateTotal : Date * seq of Transaction +> nat
DateTotal(date,ts) ==
Sum([t.amount | t in seq ts & t.date = date]);
values
dailyLimit : nat = 2000;
operations
InsertCard : Card ==> ()
InsertCard(c) ==
curCard := c
pre curCard = nil;
Validate : PinCode ==> <PinOk> | <PinNotOk> | <Retained>
Validate(pin) ==
let codeOk = curCard.code = Encode(pin),
cardLegal = IsLegalCard(curCard,illegalCards,accounts)
in
(if not cardLegal then
(retainedCards := retainedCards union {curCard};
cardOk := false;
curCard := nil;
return <Retained>)
else
cardOk := codeOk;
return if cardOk
then <PinOk>
else <PinNotOk>)
pre curCard <> nil and not cardOk;
ReturnCard : () ==> ()
ReturnCard() ==
(cardOk := false;
curCard:= nil)
pre curCard <> nil;
GetBalance : () ==> nat
GetBalance() ==
return accounts(curCard.accountId).balance
pre curCard <> nil and cardOk and IsLegalCard(curCard,illegalCards,accounts);
MakeWithdrawal : nat * Date ==> bool
MakeWithdrawal(amount,date) ==
let mk_Card(-,cardId,accountId) = curCard,
transaction = mk_Transaction(date,cardId,amount)
in
if accounts(accountId).balance - amount >= 0 and
DateTotal(date,accounts(accountId).transactions^[transaction])
<= dailyLimit
then
(accounts(accountId).balance :=
accounts(accountId).balance - amount;
accounts(accountId).transactions :=
accounts(accountId).transactions ^ [transaction];
return true)
else
return false
pre curCard <> nil and cardOk and IsLegalCard(curCard,illegalCards,accounts);
RequestStatement : () ==> Name * seq of Transaction * nat
RequestStatement() ==
let mk_Card(-,cardId,accountId) = curCard,
mk_Account(cards,balance,transactions) = accounts(accountId)
in
return mk_(cards(cardId).name,transactions,balance)
pre curCard <> nil and cardOk and IsLegalCard(curCard,illegalCards,accounts)
functions
IsLegalCard : Card * set of CardId * map AccountId to Account -> bool
IsLegalCard(mk_Card(-,cardId,accountId),pillegalcards,paccounts) ==
cardId not in set pillegalcards and
accountId in set dom paccounts and
cardId in set dom paccounts(accountId).cards;
operations
ReportIllegalCard : CardId ==> ()
ReportIllegalCard(cardId) ==
illegalCards := illegalCards union {cardId};
AddAccount : AccountId * Account ==> ()
AddAccount(accountId,account) ==
accounts := accounts munion {accountId |-> account}
pre accountId not in set dom accounts;
functions
Encode: PinCode +> Code
Encode(pin) ==
pin; -- NB The actual encoding procedure has not yet been chosen
Sum: seq of real +> real
Sum(rs) ==
if rs = [] then 0
else
hd rs + Sum(tl rs)
measure Len;
Len: seq of real +> nat
Len(list) ==
len list;
traces
TestCash: let c in set {mk_Card(1,1,1), mk_Card(2,2,2)}
in
(InsertCard(c);
Validate(1111);
ReportIllegalCard(c.cardId)){1,5};
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
