Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: System.vdmpp Sprache: VDM

Original von: VDM^©

class System

instance variables

private Purses: map Purse`CardId to Purse;
inv forall p in set dom Purses & Purses(p).GetCardNo() = p;
private Log: seq of Transaction := [];

types

public Transaction ::
         fromId : Purse`CardId
         toId   : Purse`CardId
         sum    : nat;

operations

public Transfer: Purse`CardId * Purse`CardId * nat ==> ()
Transfer(fromId, toId, sum) ==
( Purses(fromId).DecreaseBal(sum);
  Purses(toId).IncreaseBal(sum);
)
pre {fromId, toId} subset dom Purses and
    fromId <> toId and
    Purses(fromId).GetBalance() >= sum;

public System: set of Purse ==> System
System(PurseSet) ==
  Purses := {p.GetCardNo() |-> p | p in set PurseSet}
pre forall p,q in set PurseSet & p <> q => p.GetCardNo() <> q.GetCardNo();

public TotalTransferred:() ==> nat
TotalTransferred() ==
  return TotalSum(Log);

functions

TotalSum: seq of Transaction -> nat
TotalSum(tseq) ==
  if tseq = []
  then 0
  else let tx = hd tseq
       in
         tx.sum + TotalSum(tl tseq)
measure Len;

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

end System

¤ Dauer der Verarbeitung: 0.16 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.