Quelle AutomatedStockBroker.vdmpp Sprache: VDM

class AutomatedStockBroker is subclass of GLOBAL

instance variables
  stocks : seq of StockRecord;
  stockWatchers : map StockIdentifier to StockWatcher;
  actionLog : seq of ActionEvent := [];
  balance : int;
  inv balance >= 0;
  -- no stock can have the same name
  inv forall x,y in set inds stocks & x <> y => stocks(x).Name <> stocks(y).Name;

  --says that foreach ActionEvent in the log if there exist a next action with the same
  --Stock name, it should have a different ActionType. this insures that you dont sell or buy the same
  --two times in a row
  inv let stockIdentifiers = {si.Name | si in set elems stocks}
      in
        forall stockIdentifier in set stockIdentifiers &
          let allEventsStock = [ e | e in seq actionLog
                                   & e.StockName = stockIdentifier]
          in
            (forall i in set inds allEventsStock &
               (i <> len allEventsStock) =>
               (allEventsStock(i).Type <> allEventsStock(i+1).Type));

  inv MaxOneOfEachActionTypePerTime(actionLog);


operations

public AutomatedStockBroker: nat ==> AutomatedStockBroker
AutomatedStockBroker(startCash) == (
  balance := startCash;
  stocks := [];
  stockWatchers := {|->};
);

public AddStock: StockRecord * nat1 ==> ()
AddStock(sRecord,priority) == (
  stocks := stocks(1,...,priority-1) ^ [sRecord]
            ^ stocks(priority+1,...,len stocks);
  if (World`simulate)
  then stockWatchers(sRecord.Name) := new StockWatcher(sRecord)
  else stockWatchers(sRecord.Name) := new StockWatcher(sRecord,testValues(sRecord.Name));
)
pre sRecord.Name not in set { x.Name | x in seq stocks}
post (sRecord.Name in set dom stockWatchers)
     and (sRecord = stocks(priority));

public GetActionLog:() ==> seq of ActionEvent
GetActionLog() ==
  return actionLog;

public GetStocksWithActiveActionTrigger: StockState ==> seq of StockRecord
GetStocksWithActiveActionTrigger(ss) ==
  return [e | e in seq stocks
            & (stockWatchers(e.Name).GetTriggeredAction() <> nil)
              and (e.State = ss)]
post let res = RESULT in forall i in set inds res & res(i).State = ss;

pure FindValidBuy: seq of StockRecord * nat ==> [StockRecord]
FindValidBuy(potBuys,time) ==
  return let affordableStocks =
    [x | x in seq potBuys & CanAfford(x,balance)]
     in
     (
      if(len affordableStocks > 0)
      then let x in seq affordableStocks be st
       (forall y in seq affordableStocks & (stockWatchers(x.Name).GetStockValue(time)) >=
       (stockWatchers(y.Name).GetStockValue(time)))
       in x
      else nil
     );

pure FindValidSell: seq of StockRecord * nat ==> StockRecord
FindValidSell(potSells,time) ==
  return let x in seq potSells be st
    (forall y in seq potSells &
      (stockWatchers(x.Name).GetStockValue(time) - x.Cost) >=
      (stockWatchers(y.Name).GetStockValue(time) - y.Cost))
    in x
pre len potSells > 0
post IsGTAll(stockWatchers(RESULT.Name).GetStockValue(time) - RESULT.Cost,
  {stockWatchers(x.Name).GetStockValue(time) - x.Cost | x in seq potSells});

  PerformBuy: StockRecord * nat ==> ()
  PerformBuy(potAction,time) ==
   let sw = stockWatchers(potAction.Name),value = sw.GetStockValue(time)
   in
   (
    actionLog := [mk_ActionEvent(<Buy>,time,potAction.Name,value)] ^ actionLog;
    balance := balance - value;

    let i in set inds stocks be st stocks(i).Name = potAction.Name
     in
    (
     stocks(i) := mu(potAction, State |-> <Bought>, Cost |-> value );
     sw.updateStockRecord(stocks(i))
    )
   )
  pre potAction.State = <PotentialBuy> and
   stockWatchers(potAction.Name).GetTriggeredAction() = <Buy>
  post balance >= 0;

  PerformSell: StockRecord * nat ==> ()
  PerformSell(potAction,time) ==
   let sw = stockWatchers(potAction.Name),value = sw.GetStockValue(time)
   in
   (
    actionLog := [mk_ActionEvent(<Sell>,time,potAction.Name,value)] ^ actionLog;
    balance := balance + value;

    let i in set inds stocks be st stocks(i).Name = potAction.Name
     in
    (
     stocks(i) := mu(potAction, State |-> <PotentialBuy>, Cost |-> 0);
     sw.updateStockRecord(stocks(i))
    )
   )
  pre potAction.State = <Bought> and
   stockWatchers(potAction.Name).GetTriggeredAction() = <Sell>
  post balance >= 0;

  ObserveAllStocks: nat ==> ()
  ObserveAllStocks(time) ==
   for all i in set inds stocks do
    let stock = stocks(i), csw = stockWatchers(stock.Name)
     in csw.ObserveStock(time);

  public Step: nat ==> ()
  Step(time) == (

   ObserveAllStocks(time);

   let potBuys = GetStocksWithActiveActionTrigger(<PotentialBuy>) ,
    potSells = GetStocksWithActiveActionTrigger(<Bought>),
    validBuy = FindValidBuy(potBuys,time)
    in
    (
     if(len potSells > 0)
     then (PerformSell(FindValidSell(potSells,time), time);)
     else skip;
     IO`print("\npot sels : ");
     IO`print(potSells);

     if(validBuy <> nil)
     then (PerformBuy(validBuy, time);)
     else skip;
     IO`print("\npot buys : ");
     IO`print(potBuys);
    );

   IO`print("\n");
   IO`print("Finished step : ");
   IO`print(time);
   IO`print(" with actionLog : ");
   IO`print(actionLog);
   IO`print(" and Balance : ");
   IO`print(balance);
   IO`print("\n");
  )
  post MaxOneOfEachActionTypePerTime(actionLog);

functions

IsGTAll: int * set of int -> bool
IsGTAll(sv,ssv) ==
  forall i in set ssv & sv >= i;

CanAfford: StockRecord * nat -> bool
CanAfford(sr,balance) ==
  sr.Cost <= balance;

MaxOneOfEachActionTypePerTime: seq of ActionEvent -> bool
MaxOneOfEachActionTypePerTime(actionLog) ==
  forall x,y in set inds actionLog &
     (x <> y and actionLog(x).Time = actionLog(y).Time) =>
     (actionLog(x).Type <> actionLog(y).Type)

end AutomatedStockBroker

quality92%

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