products/Sources/formale Sprachen/VDM/VDMPP/CashDispenserPP image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Card.vdmpp   Sprache: VDM

Original von: 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.17 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.


Bot Zugriff