types String = seq of char inv s == s <> []; Message = String inv m == len m <= 100; Classification = | ; Category = set of String; Ports :: high: seq of Message low : seq of Message functions Occurs: String * String -> bool Occurs(substr,str) == exists i,j in set inds str & substr = str(i,...,j); Classify: Message * Category -> Classification Classify(m,cat) == if exists hi in set cat & Occurs(hi,m) then else ; Gateway: seq of Message * Category -> Ports Gateway(ms,cat) == if ms = [] then mk_Ports([],[]) else let rest_p = Gateway(tl ms,cat) in ProcessMessage(hd ms,cat,rest_p); ProcessMessage: Message * Category * Ports -> Ports ProcessMessage(m,cat,ps) == if Classify(m,cat) = then mk_Ports([m]^ps.high,ps.low) else mk_Ports(ps.high,[m]^ps.low); Gateway2: seq of Message * Category -> Ports Gateway2(ms,cat) == mk_Ports([ms(i)|i in set inds ms & Classify(ms(i),cat) = ], [ms(i)|i in set inds ms & Classify(ms(i),cat) = ]); AnyHighClass: seq of Message * Category -> bool AnyHighClass(ms,cat) == exists m in set elems ms & Classify(m,cat) = ; Censor: seq of Message * Category -> seq of Message Censor(ms,cat) == [ms(i) | i in set inds ms & Classify(ms(i),cat) = ]; FlattenMessages: seq of Message -> Message FlattenMessages(ms) == conc ms pre len conc ms <= 100