| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/CashDispenserPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 819 B |
|
Quelle Card.vdmpp Sprache: VDM |
|||||||||
|
\section{The Class Card}
This class models physical cards. Each card has a code, a card id and an account id stored on it. The class provides operations to create a card and to read information stored on a card. \begin{vdm_al} class Card types public CardId = nat; public Code = nat; public PinCode = nat; instance variables code : Code; cardId : CardId; accountId : Account`AccountId; operations public Card : Code * CardId * Account`AccountId ==> Card Card(c,cid,a) == (code := c; cardId := cid; accountId := a); pure public GetCode : () ==> Code GetCode() == return code; pure public GetAccountId : () ==> Account`AccountId GetAccountId() == return accountId; pure public GetCardId : () ==> CardId GetCardId() == return cardId; end Card \end{vdm_al} ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28