Mercurial > urweb

annotate tests/policy.ur @ 1242:4ed556678214

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
At loop heads, havoc relations that might be changed by the loop
author Adam Chlipala <adamc@hcoop.net>
date Sat, 17 Apr 2010 14:26:52 -0400
parents d5ecceb7d1a1
children
rev   line source
adamc@1204 1 type fruit = int
adamc@1204 2 table fruit : { Id : fruit, Nam : string, Weight : float, Secret : string }
adamc@1204 3 PRIMARY KEY Id,
adamc@1204 4 CONSTRAINT Nam UNIQUE Nam
adamc@1204 5
adamc@1204 6 type order = int
adamc@1204 7 table order : { Id : order, Fruit : fruit, Qty : int, Code : int }
adamc@1204 8 PRIMARY KEY Id,
adamc@1204 9 CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id)
adamc@1199 10
adamc@1207 11 (* Everyone may knows IDs and names. *)
adamc@1236 12 policy sendClient (SELECT fruit.Id, fruit.Nam
adamc@1214 13 FROM fruit)
adamc@1207 14
adamc@1207 15 (* The weight is sensitive information; you must know the secret. *)
adamc@1214 16 policy sendClient (SELECT fruit.Weight, fruit.Secret
adamc@1214 17 FROM fruit
adamc@1214 18 WHERE known(fruit.Secret))
adamc@1207 19
adamc@1214 20 policy sendClient (SELECT order.Id, order.Fruit, order.Qty
adamc@1214 21 FROM order, fruit
adamc@1214 22 WHERE order.Fruit = fruit.Id
adamc@1214 23 AND order.Qty = 13)
adamc@1200 24
adamc@1207 25 fun fname r =
adamc@1207 26 x <- queryX (SELECT fruit.Weight
adamc@1207 27 FROM fruit
adamc@1207 28 WHERE fruit.Nam = {[r.Nam]}
adamc@1210 29 AND fruit.Secret = {[r.Secret]}
adamc@1210 30 AND fruit.Weight <> 3.14
adamc@1210 31 AND fruit.Weight < 100.0
adamc@1210 32 AND fruit.Weight <= 200.1
adamc@1210 33 AND fruit.Weight > 1.23
adamc@1210 34 AND fruit.Weight >= 1.24)
adamc@1207 35 (fn r => <xml>Weight is {[r.Fruit.Weight]}</xml>);
adamc@1207 36
adamc@1207 37 return <xml><body>
adamc@1207 38 {x}
adamc@1207 39 </body></xml>
adamc@1207 40
adamc@1200 41 fun main () =
adamc@1204 42 x1 <- queryX (SELECT fruit.Id, fruit.Nam
adamc@1209 43 FROM fruit
adamc@1210 44 WHERE fruit.Nam = "apple")
adamc@1204 45 (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
adamc@1204 46
adamc@1204 47 x2 <- queryX (SELECT fruit.Nam, order.Qty
adamc@1204 48 FROM fruit, order
adamc@1206 49 WHERE fruit.Id = order.Fruit
adamc@1206 50 AND order.Qty = 13)
adamc@1204 51 (fn x => <xml><li>{[x.Fruit.Nam]}: {[x.Order.Qty]}</li></xml>);
adamc@1200 52
adamc@1228 53 ro <- oneOrNoRows (SELECT fruit.Id, fruit.Nam
adamc@1228 54 FROM fruit);
adamc@1228 55
adamc@1200 56 return <xml><body>
adamc@1204 57 <ul>{x1}</ul>
adamc@1210 58
adamc@1204 59 <ul>{x2}</ul>
adamc@1207 60
adamc@1228 61 {case ro of
adamc@1228 62 None => <xml>None</xml>
adamc@1228 63 | Some _ => <xml>Some</xml>}
adamc@1228 64
adamc@1207 65 <form>
adamc@1207 66 Fruit name: <textbox{#Nam}/><br/>
adamc@1207 67 Secret: <textbox{#Secret}/><br/>
adamc@1207 68 <submit action={fname}/>
adamc@1207 69 </form>
adamc@1200 70 </body></xml>