fact: Definition BookStoreSpec : ADT _ := Def ADT { rep := QueryStructure BookStoreSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "PlaceOrder" ( r : rep) (o : Order) : rep * bool := Insert o into r!sORDERS, Def Method1 "AddBook" (r : rep) (b : Book) : rep * bool := Insert b into r!sBOOKS , Def Method1 "GetTitles" (r : rep) (author : W) : rep * list W := titles <- For (b in r ! sBOOKS) Where (author = b!sAUTHOR) Return (b!sTITLE); ret (r, titles), Def Method1 "NumOrders" (r : rep) (author : W ) : rep * W := count <- Count (For (o in r!sORDERS) (b in r!sBOOKS) Where (author = b!sAUTHOR) Where (o!sISBN = b!sISBN) Return ()); ret (r, Word.natToWord 32 count) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory