fact: Definition StocksSpec : ADT _ := Def ADT { rep := QueryStructure StocksSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddStock" (r : rep) (stock: StocksSchema#STOCKS) : rep * bool := Insert stock into r!STOCKS, Def Method1 "AddTransaction" (r : rep) (transaction : StocksSchema#TRANSACTIONS) : rep * bool := Insert transaction into r!TRANSACTIONS, Def Method2 "TotalVolume" (r : rep) (code : StockCode) (date : Date) : rep * W := sum <- SumW (For (transaction in r!TRANSACTIONS) Where (transaction!STOCK_CODE = code) Where (transaction!DATE = date) Return transaction!VOLUME); ret (r, sum), Def Method2 "MaxPrice" (r : rep) (code : StockCode) (date : Date) : rep * option W := max <- MaxW (For (transaction in r!TRANSACTIONS) Where (transaction!STOCK_CODE = code) Where (transaction!DATE = date) Return transaction!PRICE); ret (r, max), Def Method2 "TotalActivity" (r : rep) (code : StockCode) (date : Date) : rep * W := count <- Count (For (transaction in r!TRANSACTIONS) Where (transaction!STOCK_CODE = code) Where (transaction!DATE = date) Return ()); ret (r, Word.natToWord 32 count), Def Method2 "LargestTransaction" (r : rep) (type : StockType) (date : Date) : rep * option W := max <- MaxW (For (stock in r!STOCKS) (transaction in r!TRANSACTIONS) Where (stock!TYPE = type) Where (transaction!DATE = date) Where (stock!STOCK_CODE = transaction!STOCK_CODE) Return (Word.wmult transaction!PRICE transaction!VOLUME)); ret (r, max) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory