fact: Definition SmtpSpec : ADT SmtpSig := Def ADT { rep := QueryStructure ConnectionSchema, Def Constructor "Init" (_: unit) : rep := empty,, query "GetState" (r : rep, id: UUID) : option State := q <- (For (c in r!sCONNECTIONS) Where (id = c!sID) Return (c!sSTATE)); ret (hd_error q), query "GetConnection" (r : rep, id: UUID) : option Connection := q <- (For (c in r! sCONNECTIONS) For (c in r! sCONNECTIONS) Where (id = c!sID) Return (c)); ret (hd_error q), update "AddConnection" (r : rep, conn: Connection) : bool := Insert conn into r!sCONNECTIONS, update "KillConnection" (r : rep, id: UUID) : bool := q <- Delete c from r!sCONNECTIONS where c!sID = id; let (updated, deleted) := q in ret (updated, nonEmpty deleted), update "Helo" (r : rep, arg: UUID * string) : Reply := let (id, domain) := arg in q <- Update c from r!sCONNECTIONS as d making (d!sSTATE = S_Mail /\ d!sDOMAIN = domain) where (c!sID = id /\ c!sSTATE = S_Helo); let (updated, affected) := q in ret (updated, standardReplyExists(affected)), update "Mail" (r : rep, arg: UUID * string) : Reply := let (id, mailfrom) := arg in q <- Update c from r!sCONNECTIONS as c' making c!sSTATE = S_Rcpt /\ c!sMAILFROM = mailfrom where (c!sID = id /\ c!sSTATE = S_Mail); let (updated, affected) := q in ret (updated, standardReplyExists(affected)), update "Rcpt" (r : rep, arg: UUID * string) : Reply := let (id, rcptto) := arg in q <- Update c from r!sCONNECTIONS as c' making c'!sRCPTTO = rcptto :: c!sRCPTTO where (c!sID = id /\ c!sSTATE = S_Rcpt); let (updated, affected) := q in ret (updated, standardReplyExists(affected)), update "Data" (r : rep, id: UUID) : Reply := q <- Update c from r!sCONNECTIONS as c' making c'!sSTATE = S_Data where (c!sID = id /\ c!sSTATE = S_Rcpt /\ nonEmpty(c!sRCPTTO) = true); let (updated, affected) := q in ret (updated, standardReplyExists(affected)), update "MoreData" (r : rep, arg: UUID * string) : Reply := let (id, data) := arg in q <- Update c from r!sCONNECTIONS as c' making c'!sBODY = append data c!sBODY where (c!sID = id /\ c!sSTATE = S_Data); let (updated, affected) := q in ret (updated, standardReplyExists(affected)), update "Rset" (r : rep, id: UUID) : bool := q <- Update c from r!sCONNECTIONS as c' making c'!sSTATE = S_Mail /\ c'!sMAILFROM = "" /\ c'!sRCPTTO = @nil string /\ c'!sBODY = "" where (c!sID = id /\ c!sSTATE <> S_Helo /\ c!sSTATE <> S_Inactive); let (updated, affected) := q in ret (updated, nonEmpty(affected)), update "Quit" (r : rep, id: UUID) : bool := q <- Update c from r!sCONNECTIONS as c' making (c'!sSTATE = S_Inactive /\ c'!sMAILFROM = "" /\ c'!sRCPTTO = @nil string /\ c'!sBODY = "") where (c!sID = id); let (updated, affected) := q in ret (updated, nonEmpty(affected)) }.
imports: Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT