(* <pre> *)
(**************************************************************************
 ***  Kurt Mammen
 ***  CSC 590 - Fall 1994
 ***  A Formal Specification of My Thesis in RSL -- A User's View
 *************************************************************************)

(*-----------------------------------------------------------------------*)
(*--- A X I O M S -------------------------------------------------------*)
(*-----------------------------------------------------------------------*)

(*-------------------------------------------------------------------------
The CrossOverRate is a parameter to the OptimizeSecurity operation.  It
is set by the user and affects the performance of the genetic algorithm.
-------------------------------------------------------------------------*)
object CrossOverRate =  number;
    axiom A1 = forall( r:CrossOverRate ) ( (r >= 0) and (r <= 1) );

(*-------------------------------------------------------------------------
The MutationRatee is a parameter to the OptimizeSecurity operation.  It
is set by the user and affects the performance of the genetic algorithm.
-------------------------------------------------------------------------*)
object MutationRate =  number;
    axiom A2 = forall( r:MutationRate ) ( (r >= 0) and (r <= 1) );

(*-------------------------------------------------------------------------
A Signal is the type of value returned by the operation GetSecuritySignal.
It is a fuzzy buy-sell signal.
-------------------------------------------------------------------------*)
object Signal =  string;
   axiom A3 = forall( s:Signal )
      ( (s = "Weak Buy")  or (s = "Buy")  or (s = "Strong Buy")  or
        (s = "Weak Sell") or (s = "Sell") or (s = "Strong Sell") or
        (s = "Neutral")
      );

(*-------------------------------------------------------------------------
The TimePeriod is a parameter to the GetSecurityReturn operation.  It
provided by the user and specifies the period of time over which the
annualized rate-of-return is calculated.
-------------------------------------------------------------------------*)
object TimePeriod =  string;
   axiom A4 = forall( p:TimePeriod )
      ( (p = "One Week")   or (p = "One Month") or (p = "Three Months") or
        (p = "Six Months") or (p = "One Year")
      );
 
(*-----------------------------------------------------------------------*)
(*--- O B J E C T S -----------------------------------------------------*)
(*-----------------------------------------------------------------------*)
object FileSystem
   description: (*
      A permanent data store for Portfolios objects.
   *);
   components:
      Portfolios:Portfolio*;
end FileSystem;
 
object MarketData
   description: (*
      Daily price and volume data for a security or index.
   *);
   components:
      Symbol:string,         (* Unique identifier *)
      Date:number,           (* Date of the data *)
      Open:number,           (* Opening price *)
      High:number,           (* Intraday high price *)
      Close:number,          (* Closing price *)
      Volume:number;         (* Trading volume *)
end MarketData;

object MarketHistory
   description: (*
      A collection of MarketData objects over time.
   *);
   components:
      History:MarketData*;
end MarketHistory;

object Portfolio
   description: (*
      A named collection of Security objects.
   *);
   components:
      Name:string,
      Securities:Security*;
end Portfolio;

object Security
   description: (*
      A Security is a named combination of a security symbol and a Trading-
      Rule.  The symbol identifies the appropriate MarketData to use when
      optimizing the TradingRule.
   *);
   components:
      Name:string,           (* A unique, user-supplied, identifier *)
      Symbol:string,         (* The security or index symbol *)
      Rule:TradingRule;      (* The trading rule to optimize *)
end Security;

object TradingRule
   description: (*
      A TradingRule is a rule for determining when to buy or sell a
      security.  It is expressed in a way that allows it to be optimized
      using genetic algorithms.  Note that a TradingRule is not associated
      with a particular security, and that it cannot be optimized until it
      is associated with the market history of a specific security through
      a Security object.
   *);
   components:
      Name:string;           (* A unique rule identifier *)
end TradingRule;

object TradingRules
   description: (* 
      A permanent data store for TradingRule objects.
   *);
   components:
      TradingRule*;
end TradingRules;

(*-----------------------------------------------------------------------*)
(*--- P O R T F O L I O  O P E R A T I O N S ----------------------------*)
(*-----------------------------------------------------------------------*)
operation CreatePortfolio 
   description: (*
      Creates a new named Portfolio object.  The new Portfolio will contain
      no Securites.
   *);
   inputs:
      Name:string;
   outputs:
      p':Portfolio;
end CreatePortfolio;

operation DeletePortfolio 
   description: (*
      Deletes a Portfolio from the FileSystem.
   *);
   inputs:
      fs:FileSystem, Name:string;
   outputs:
      fs':FileSystem;
end DeletePortfolio;

operation OpenPortfolio 
   description: (*
      Retrieves an existing Portfolio from the FileSystem.
   *);
   inputs:
      fs:FileSystem, Name:string;
   outputs:
      p':Portfolio;
end OpenPortfolio;

operation SavePortfolio 
   description: (*
      Saves a Portfolio to the FileSystem.
   *);
   inputs:
      fs:FileSystem, p:Portfolio;
   outputs:
      fs':FileSystem;
end SavePortfolio;

operation SaveAsPortfolio 
   description: (*
      Changes the name of the Portfolio and saves it in the FileSystem.
   *);
   inputs:
      fs:FileSystem, p:Portfolio, Name:string;
   outputs:
      fs':FileSystem, p':Portfolio;
end SaveAsPortfolio;

(*-----------------------------------------------------------------------*)
(*--- S E C U R I T Y   O P E R A T I O N S -----------------------------*)
(*-----------------------------------------------------------------------*)
operation CreateSecurity 
   description: (*
      Create a new Security object, makes it availible for manipulation,
      and places it in the Portfolio.
   *);
   inputs:
       p:Portfolio, SecurityName:string, Symbol:string, h:MarketHistory,
       RuleName:string, Rules:TradingRules;
   outputs:
      p':Portfolio, s':Security;
end CreateSecurity;

operation DeleteSecurity 
   description: (*
      Deletes a Security from a Portfolio.
   *);
   inputs:
      p:Portfolio, Name:string;
   outputs:
      p':Portfolio;
end DeleteSecurity;

operation GetSecurityReturn 
   description: (*
      Returns the annualized rate-of-return for the period of time
      specified.  The rate-of-return is determined by following the
      buy-sell signals generated by the TradingRule associated with the
      Security and calculating the gain or loss from the MarketHistory.
   *);
   inputs:
      s:Security, h:MarketHistory, TimePeriod:number;
   outputs:
      Return':number;
end GetSecurityReturn;

operation GetSecuritySignal 
   description: (*
      Returns the current Buy-Sell signal for the specified security
      based on its market history.
   *);
   inputs:
      s:Security, h:MarketHistory;
   outputs:
      s':Signal;
end GetSecuritySignal;

operation OpenSecurity 
   description: (*
      Selects the specified Security from a Portfolio and makes it
      availible for manipulation.
   *);
   inputs: p:Portfolio, Name:string;
   outputs: s':Security;
end OpenSecurity;

operation OptimizeSecurity 
   description: (*
      OptimizeSecurity is the workhorse of the system.  It applies 
      genetic algorithm techniques to a Security to find an optimal
      or near-optimal TradingRule over its associated MarketHistory.
      The PopulationSize, NumberOfPopulations, NumberOfGenerations,
      CrossOverRate, and MutationRate are all parameters supplied by
      the user that affect the performance of the genetic algorithm.
   *);
   inputs: s:Security, h:MarketHistory, PopulationSize:number,
           NumberOfPopulations:number, NumberOfGenerations:number,
           cr:CrossOverRate, mr:MutationRate;
   outputs:
      s':Security;
end OptimizeSecurity;

operation SetSecurityName 
   description: (*
      Changes the name of a Security to the new value and puts the modified
      Security in the Portfolio.
   *);
   inputs: p:Portfolio, s:Security, Name:string;
   outputs: p':Portfolio, s':Security;
end SetSecurityName;

operation SetSecurityRule 
   description: (*
      Changes the rule of a Security to the new TradingRule and puts the
      modified Security in the Portfolio.
   *);
   inputs: p:Portfolio, s:Security, RuleName:string, r:TradingRules;
   outputs: p':Portfolio, s':Security;
end SetSecurityRule;

operation SetSecuritySymbol
   description: (*
      Changes the symbol of a Security to the new value and puts the
      modified Security in the Portfolio.
   *);
   inputs: p:Portfolio, s:Security, Symbol:string, h:MarketHistory;
   outputs: p':Portfolio, s':Security;
end SetSecuritySymbol;