(**************************************************************************
 ***  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 =  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 name.  The symbol identifies the appropriate MarketData to use when
      optimizing the TradingRule.  The Trading Rule name identifies which
      TradingRule to use.
   *);
   components:
      Name:string,           (* A unique, user-supplied, identifier *)
      Symbol:string,         (* The security or index symbol *)
      Rule:string;           (* Name of 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 (* and *) ;
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;
   precondition:
      not exists (p:Portfolio) (p.Name = Name);
   postcondition:
      (p'.Name = Name);
end CreatePortfolio;

operation DeletePortfolio
   description: (*
      Deletes a Portfolio from the FileSystem.
   *);
   inputs:
      fs:FileSystem, Name:string;
   outputs:
      fs':FileSystem;
   precondition:
      exists (p:Portfolio)
      (
         (p.Name = Name) and (p in fs)
      );
   postcondition:
      not exists (p':Portfolio)
      (
         (p'.Name = Name) and (p' in fs')
      );
end DeletePortfolio;

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

operation SavePortfolio
   description: (*
      Saves a Portfolio to the FileSystem.
   *);
   inputs:
      fs:FileSystem, p:Portfolio;
   outputs:
      fs':FileSystem;
   precondition:;
   postcondition:
      (p in fs');
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;
   precondition:
      not exists (p'':Portfolio)
      (
         (p''.Name = Name) and (p'' in fs)
      );
   postcondition:
      (p'.Name = Name) and (p' in fs');
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, History:MarketHistory,
      RuleName:string, Rules:TradingRules;
   outputs:
      p':Portfolio, s':Security;
   precondition:
      (
         not exists (s:Security)
         (
            (SecurityName = s.Name) and (s in p.Securities)
         )
         and exists (d:MarketData)
         (
            (d.Symbol = Symbol) and (d in History)
         )
         and exists (r:TradingRule)
         (
            (r.Name = RuleName) and (r in Rules)
         )
      );
   postcondition:
      (s' in p'.Securities)
      and (s'.Name   = SecurityName)
      and (s'.Symbol = Symbol)
      and (s'.Rule   = RuleName);
end CreateSecurity;

operation DeleteSecurity
   description: (*
      Deletes a Security from a Portfolio.
   *);
   inputs:
      p:Portfolio, Name:string;
   outputs:
      p':Portfolio;
   precondition:
      exists (s:Security)
      (
         (s in p.Securities) and (s.Name = Name)
      );
   postcondition:
      not exists (s':Security)
      (
         (s'.Name = Name) and (s' in p'.Securities)
      );
end DeleteSecurity;

operation GetSecurityReturn
   description: (*
      Returns the annualized rate-of-return for the period of time
      specified.  See the function CalculateAnnualizedReturn() below.
   *);
   inputs:
      s:Security, h:MarketHistory, t:TimePeriod;
   outputs:
      Return':number;
   precondition:;
   postcondition:
      Return' = CalculateAnnualizedReturn(s,h,t);
end GetSecurityReturn;

(* 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.  This function begins to leave
 * the external user-view and enter the genetic algorithm/fuzzy logic
 * internal view -- so it implementation is opaque.
 *)
function CalculateAnnualizedReturn(s:Security, h:MarketHistory, t:TimePeriod)
      -> (number) = ...;

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

(* The Buy-Sell signal is generated by evaluating the genetic algorithm 
 * rule.  This function begins to leave the external user-view and enter
 * the internal-view -- so its implementation is opaque.
 *) 
function GenerateSignal(s:Security, h:MarketHistory) -> (Signal) = ...;

operation OpenSecurity
   description: (*
      Selects the specified Security from a Portfolio and makes it
      availible for manipulation.
   *);
   inputs:
      p:Portfolio, Name:string;
   outputs:
      s':Security;
   precondition:
      exists (s:Security)
      (
         (s in p.Securities)
         and (s.Name = Name)
      );
   postcondition:
      (* KDMTODO ????? *);
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:
      p:Portfolio, s:Security, h:MarketHistory, PopulationSize:number,
      NumberOfPopulations:number, NumberOfGenerations:number,
      cr:CrossOverRate, mr:MutationRate;
   outputs:
      p':Portfolio, s':Security;
   (* KDMTODO - How do I do pre and post for this? *)
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;
   precondition:
      not exists (s'':Security)
      (
         (s''.Name = Name)
         and (s'' in p.Securities)
      );
   postcondition:
      exists (s'':Security)
      (
         (s' in p'.Securities)
         and (s'.Name   = Name)
         and (s'.Symbol = s.Symbol)
         and (s'.Rule   = s.Rule)
      );
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, Rules:TradingRules;
   outputs:
      p':Portfolio, s':Security;
   precondition:
      (
         (s in p.Securities)
         and exists (r:TradingRule)
         (
            (r.Name = RuleName)
            and (r in Rules)
         )
      );
   postcondition:
      (
         (s' in p'.Securities) 
         and (s'.Name   = s.Name)
         and (s'.Symbol = s.Symbol)
         and (s'.Rule   = RuleName)
      );
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, History:MarketHistory;
   outputs:
      p':Portfolio, s':Security;
   precondition:
      (
         (s in p.Securities)
         and exists (d:MarketData)
         (
            (d.Symbol = Symbol)
            and (d in History)
         )
      );
   postcondition:
      (
         (s' in p'.Securities)
         and (s'.Name   = s.Name)
         and (s'.Symbol = Symbol)
         and (s'.Rule   = s.Rule)
      );
end SetSecuritySymbol;