Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Account.vdmpp Sprache: VDM

Original von: VDM^©

\section{The Class Account}

This class models an account. A number of cards held by individual
cardholders are associated with an account. An account has a balance
and records transactions.

\begin{vdm_al}
class Account

instance variables
  cards : map Card`CardId to Cardholder;
  balance : nat;
  transactions : seq of Transaction := [];

  inv TransactionsInvariant(transactions);
\end{vdm_al}

The invariant ensures that transactions performed on the same day do
not exceed the daily limit, which is a constant value defined
below. Note that we have chosen to not allow a negative balance.

\begin{vdm_al}
values
  dailyLimit : nat = 2000;

types
  public AccountId = nat;
  public Transaction :: date : Clock`Date
                 cardId : Card`CardId
                 amount : nat;
\end{vdm_al}

In this specification we have chosen to model transaction as a
type. Alternatively it could have been modeled as a class, but it has
no obvious functionality except trivial read/write
operations. Moreover, transaction objects/values do not need to be
shared among many objects. Our choice also illustrates the power of
the VDM++ type system.

\begin{vdm_al}
operations
  ValidTransaction : Transaction ==> bool
  ValidTransaction(transaction) ==
    is not yet specified;

public Create : map Card`CardId to Cardholder * nat ==> Account
  Create(cs,b) ==
    (cards := cs;
     balance := b;
     return self);

  pure public GetBalance : () ==> nat
  GetBalance() ==
    return balance;
\end{vdm_al}

The Withdrawal operation checks that an account and the daily limit
are not overdrawn.

\begin{vdm_al}
  public Withdrawal : Card`CardId * nat * Clock`Date ==> bool
  Withdrawal(cardId,amount,date) ==
    let transaction = mk_Transaction(date,cardId,amount)
    in
      if balance - amount >= 0 and
         DateTotal(date,transactions^[transaction]) <= dailyLimit
      then
       (balance := balance - amount;
        transactions := transactions ^ [transaction];
        return true)
      else
        return false
  pre cardId in set dom cards;

  public MakeStatement : Card`CardId * Clock`Date ==> Letter
  MakeStatement(cardId,date) ==
    let nm = cards(cardId).GetName(),
        addr = cards(cardId).GetAddress()
    in
      (dcl letter : Letter := new Letter();
       letter.Create(nm,addr,date,transactions,balance))
  pre cardId in set dom cards;
\end{vdm_al}

The GetCardIds operation is used to obtain all cards associated with the account.
\begin{vdm_al}
  pure public GetCardIds: () ==> set of Card`CardId
  GetCardIds() ==
    return dom cards;
\end{vdm_al}

The following operations and functions provide auxiliary functionality of various sorts.

\begin{vdm_al}
  public AddCard : Card`CardId * Cardholder ==> ()
  AddCard(cId,ch) ==
    cards := cards munion {cId |-> ch}
  pre cId not in set dom cards;

  public RemoveCard : Card`CardId ==> ()
  RemoveCard(cId) ==
    cards := {cId} <-: cards
  pre cId in set dom cards;

functions
  TransactionsInvariant: seq of Transaction +> bool
  TransactionsInvariant(ts) ==
    forall date in set {t.date | t in seq ts} &
      DateTotal(date,ts) <= dailyLimit;
\end{vdm_al}

The transactions invariant first computes all dates in the sequence of transactions and then compares the sum of the drawn amounts for each day with the daily limit.

\begin{vdm_al}
  DateTotal : Clock`Date * seq of Transaction +> nat
  DateTotal(date,ts) ==
    Sum([t.amount | t in seq ts & t.date = date]);

  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;

end Account
\end{vdm_al}

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.