Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Mainboard.pas.~975~ Sprache: VDM

Original von: VDM^©

\section{The Class CentralResource}

This class models the central resource. We assume there is only one
central resource in the system, though many tills can be connected to
this. The central resource holds the accounts, ids of illegal cards,
and connections to a clock and a letterbox.

\begin{vdm_al}
class CentralResource

instance variables
  accounts      : map Account`AccountId to Account := {|->};
  numberOfTries : map Card`CardId to nat := {|->};
  illegalCards  : set of Card`CardId := {};
inv dom numberOfTries union illegalCards subset
    dunion {acc.GetCardIds() | acc in set rng accounts};

  letterbox     : Letterbox;
  clock         : Clock;
\end{vdm_al}

All cards for different accounts cannot be overlapping.

\begin{vdm_al}
  inv forall acc1,acc2 in set rng accounts &
          acc1 <> acc2 =>
          acc1.GetCardIds() inter acc2.GetCardIds() = {};

values
  maxNumberOfTries : nat = 3;

operations
  public AddLetterbox : Clock * Letterbox ==> ()
  AddLetterbox(c,l) ==
    (clock := c;
     letterbox := l);
\end{vdm_al}

The following three operations provide the functionality requested in
the requirements specification of the system. The operations first
check that the requested functionality is allowed and then hand the
actual processing over to each account. Note that the checks are
necessary even though the till may have performed them as well. For
example, a card may have been reported stolen or illegal in another
way while it is being used at a till.

\begin{vdm_al}
  pure public GetBalance : Account`AccountId ==> [nat]
  GetBalance(accountId) ==
    if accountId in set dom accounts then
      accounts(accountId).GetBalance()
    else
      return nil;

  public Withdrawal : Account`AccountId * Card`CardId * nat ==> bool
  Withdrawal(accountId,cardId,amount) ==
    if IsLegalCard(accountId,cardId) then
      accounts(accountId).Withdrawal(cardId,amount,clock.GetDate())
    else
      return false;

  public PostStatement : Account`AccountId * Card`CardId ==> bool
  PostStatement(accountId,cardId) ==
    if IsLegalCard(accountId,cardId) then
      (letterbox.PostStatement
        (accounts(accountId).MakeStatement(cardId,clock.GetDate()));
       return true)
    else
      return false;
\end{vdm_al}

Next some operations follow to check whether cards are legal and
administrate number of tries stored for each card.

\begin{vdm_al}
  pure public IsLegalCard : Account`AccountId * Card`CardId ==> bool
  IsLegalCard(accountId,cardId) ==
    return
      cardId not in set illegalCards and
      accountId in set dom accounts and
      cardId in set accounts(accountId).GetCardIds();

  pure public NumberOfTriesExceeded : Card`CardId ==> bool
  NumberOfTriesExceeded(cardId) ==
    return numberOfTries(cardId) >= maxNumberOfTries;

  public ResetNumberOfTries : Card`CardId ==> ()
  ResetNumberOfTries(cardId) ==
    numberOfTries(cardId) := 0;

  public IncrNumberOfTries : Card`CardId ==> ()
  IncrNumberOfTries(cardId) ==
    numberOfTries(cardId) := numberOfTries(cardId) + 1;
\end{vdm_al}

The two operations below are used to update the central resource.

\begin{vdm_al}
  public AddAccount : Account`AccountId * Account ==> ()
  AddAccount(accId,acc) ==
    atomic
    (accounts := accounts ++ {accId |-> acc};
     numberOfTries := numberOfTries ++
                      {cId |-> 0 | cId in set acc.GetCardIds()};
     )
  pre accId not in set dom accounts;

  public AddIllegalCard : Card`CardId ==> ()
  AddIllegalCard(cId) ==
    illegalCards := illegalCards union {cId};

end CentralResource
\end{vdm_al}

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.