| products/sources/formale sprachen/Isabelle/HOL/Algebra/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: license.rtf Sprache: Unknown
|
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 [ Verzeichnis aufwärts0.18unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ] |