Quelle Purse.vdmpp Sprache: VDM

class Purse

types
public CardId = token

instance variables

private balance: nat;
private cardNo: CardId;

operations

public IncreaseBal: nat ==> ()
IncreaseBal(sum)==
  balance := balance + sum;

public DecreaseBal: nat ==> ()
DecreaseBal(sum)==
  balance := balance - sum
pre sum <= balance;

pure public GetBalance:() ==> nat
GetBalance() ==
  return balance;

pure public GetCardNo: () ==> CardId
GetCardNo() ==
  return cardNo;

public Purse: CardId * nat ==> Purse
Purse(newId, startbal) ==
( cardNo := newId;
  balance := startbal ) ;

functions
-- no functions currently defined
end Purse

quality90%

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