Quelle AccountSys.vdmsl Sprache: VDM

types

AccNum = token;

Date = token;

Details = token;

TransactionType = <Withdrawal> | <Deposit>;

Transaction ::
  date             : Date
  amount           : real
  transaction_type : TransactionType
inv mk_Transaction(-,a,-) == a > 0;

Account ::
   number  : AccNum
   details : Details
   balance : real
   limit   : real
   transactions : seq of Transaction
inv mk_Account(-,-,b,l,t) == l >= 0 and b >= l and balanceOf(t) = b

state AccountSys of
  accounts : map AccNum to Account
inv mk_AccountSys(a) == forall num in set dom a & num = a(num).number
init ac == ac = mk_AccountSys({|->})
end

functions

balanceOf: seq of Transaction -> real
balanceOf(transln) ==
  let dep   = [t.amount | t in seq transln & t.transaction_type = <Deposit>],
      withd = [t.amount | t in seq transln & t.transaction_type = <Withdrawal>]
  in
    sum(dep) - sum(withd);

sum: seq of real -> real
sum(seqln) ==
   if seqln = []
   then 0
   else hd seqln + sum(tl seqln)
measure Len;

Len: seq of real -> nat
Len(l) == len l;

operations

addAccount(numberIn: AccNum, detailsIn: Details, limitIn: real)
ext wr accounts: map AccNum to Account
pre numberIn not in set dom accounts and limitIn >= 0
post accounts = accounts~ munion {numberIn |-> mk_Account(numberIn, detailsIn, 0, limitIn,[])};

removeAccount(numberIn: AccNum)
ext wr accounts: map AccNum to Account
pre numberIn in set dom accounts
post accounts = {numberIn} <-: accounts~;

deposit(numberIn: AccNum, dateIn: Date, amountIn: real)
ext wr accounts: map AccNum to Account
pre numberIn in set dom accounts and amountIn >= 0
post let bal = accounts~(numberIn).balance,
          trans = accounts~(numberIn).transactions
      in
        let newTrans = mk_Transaction(dateIn, amountIn, <Deposit>)
        in
          accounts = accounts~ ++ {numberIn |-> mu(accounts~(numberIn),
                                                   balance |-> bal + amountIn,
                                                   transactions |-> trans ^ [newTrans])};

withdraw(numberIn: AccNum, dateIn: Date, amountIn: real)
ext wr accounts: map AccNum to Account
pre numberIn in set dom accounts and amountIn >= 0 and
    accounts(numberIn).balance -amountIn >= accounts(numberIn).limit
post let bal = accounts~(numberIn).balance,
         trans = accounts~(numberIn).transactions
     in
       let newTrans = mk_Transaction(dateIn, amountIn, <Withdrawal>)
       in
         accounts = accounts~ ++ {numberIn |-> mu(accounts~(numberIn),
                                                  balance |-> bal - amountIn,
                                                  transactions |-> trans ^ [newTrans])};

changeDetails(numberIn: AccNum, detailsIn: Details)
ext wr accounts: map AccNum to Account
pre numberIn in set dom accounts
post accounts = accounts~ ++ {numberIn |-> mu(accounts~(numberIn),details |-> detailsIn)};

changeLimits(numberIn: AccNum, limitIn: real)
ext wr accounts: map AccNum to Account
pre numberIn in set dom accounts and limitIn >= 0 and
    accounts(numberIn).balance >= limitIn
post accounts = accounts~ ++ {numberIn |-> mu(accounts~(numberIn),limit |-> limitIn)};

getDetails(numberIn: AccNum) detailsOut: Details
ext rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post detailsOut = accounts(numberIn).details;

getBalance(numberIn: AccNum) balanceOut: real
ext rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post balanceOut = accounts(numberIn).balance;

getLimit(numberIn: AccNum) limitOut: real
ext rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post limitOut = accounts(numberIn).limit;

getAllTransactions(numberIn: AccNum) transactionsOut: seq of Transaction
ext rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post transactionsOut = accounts(numberIn).transactions;

contains(numberIn: AccNum) query: bool
ext rd accounts: map AccNum to Account
post query <=> numberIn in set dom accounts;

isEmpty() query: bool
ext rd accounts: map AccNum to Account
post query <=> accounts = {|->};

getTotal() totalOut: nat
ext rd accounts: map AccNum to Account
post totalOut = card dom accounts

quality99%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

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.