Quelle GLOBAL.vdmpp Sprache: 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

quality90%

¤ 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.