Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: GLOBAL.vdmpp Sprache: VDM

Original von: VDM^©

class GLOBAL
types
public String = seq of char;

public EventType = <UpperLimit> | <LowerLimit> | <Peak> | <Valley> |
<EntersNoActionRegion> | <LeavesNoActionRegion>;

public StockState = <PotentialBuy> | <Bought>;

public Event :: Type : EventType
TimeStamp : nat
Value : nat;

public Region :: UpperValue : StockValue
  LowerValue : StockValue
inv mk_Region(p1,p2) == p1 >= p2;

public StockValue = nat;
public StockIdentifier = token;

public ActionType = <Buy> | <Sell> ;

public ActionTrigger :: Trigger : seq of EventType
Action : ActionType;

public StockRecord :: Name : StockIdentifier
Triggers : map StockState to ActionTrigger
NoActionReg : Region
Cost : StockValue
State : StockState

inv mk_StockRecord(p1,p2,p3,p4,p5) == p2(<PotentialBuy>).Action = <Buy>
and p2(<Bought>).Action = <Sell>;

public ActionEvent :: Type : ActionType
  Time : nat
  StockName : StockIdentifier
  Value : StockValue;

values
public static testValues : map StockIdentifier to seq of Event =
{mk_token("test") |-> [
mk_Event(<LeavesNoActionRegion>,6,5),
mk_Event(<LowerLimit>,5,8),
mk_Event(<UpperLimit>,4,12),
mk_Event(<EntersNoActionRegion>,3,11),
mk_Event(<LeavesNoActionRegion>,2,13),
mk_Event(<UpperLimit>,1,12),
mk_Event(<EntersNoActionRegion>,0,10)
],
mk_token("test12") |-> [
mk_Event(<LeavesNoActionRegion>,6,5),
mk_Event(<LowerLimit>,5,8),
mk_Event(<UpperLimit>,4,12),
mk_Event(<EntersNoActionRegion>,3,11),
mk_Event(<LeavesNoActionRegion>,2,16),
mk_Event(<UpperLimit>,1,12),
mk_Event(<EntersNoActionRegion>,0,10)
],
mk_token("test2") |-> [
mk_Event(<LeavesNoActionRegion>,6,5),
mk_Event(<UpperLimit>,5,8),
mk_Event(<LowerLimit>,4,8),
mk_Event(<EntersNoActionRegion>,3,11),
mk_Event(<LeavesNoActionRegion>,2,6),
mk_Event(<LowerLimit>,1,8),
mk_Event(<EntersNoActionRegion>,0,10)
]};

end GLOBAL

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