| products/sources/formale sprachen/Isabelle/Tools/jEdit/src/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: k2sea Sprache: VDMUntersuchung 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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.37Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
