Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/ElectronicPursePP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

Quelle System.vdmpp Sprache: VDM

class System

instance variables

private Purses: map Purse`CardId to Purse;
inv forall p in set dom Purses & Purses(p).GetCardNo() = p;
private Log: seq of Transaction := [];

types

public Transaction ::
         fromId : Purse`CardId
         toId   : Purse`CardId
         sum    : nat;

operations

public Transfer: Purse`CardId * Purse`CardId * nat ==> ()
Transfer(fromId, toId, sum) ==
( Purses(fromId).DecreaseBal(sum);
  Purses(toId).IncreaseBal(sum);
)
pre {fromId, toId} subset dom Purses and
    fromId <> toId and
    Purses(fromId).GetBalance() >= sum;

public System: set of Purse ==> System
System(PurseSet) ==
  Purses := {p.GetCardNo() |-> p | p in set PurseSet}
pre forall p,q in set PurseSet & p <> q => p.GetCardNo() <> q.GetCardNo();

public TotalTransferred:() ==> nat
TotalTransferred() ==
  return TotalSum(Log);

functions

TotalSum: seq of Transaction -> nat
TotalSum(tseq) ==
  if tseq = []
  then 0
  else let tx = hd tseq
       in
         tx.sum + TotalSum(tl tseq)
measure Len;

Len: seq of Transaction -> nat
Len(l) ==
  len l;

end System

quality97%

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