annotate tests/policy.ur @ 1228:7dfa67560916

Using multiple policies to check a written value
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 16:46:38 -0400
parents 648e6b087dfb
children d5ecceb7d1a1
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@1228 12 policy sendClient (SELECT fruit.Id
adamc@1228 13 FROM fruit)
adamc@1228 14 policy sendClient (SELECT fruit.Nam
adamc@1214 15 FROM fruit)
adamc@1207 16
adamc@1207 17 (* The weight is sensitive information; you must know the secret. *)
adamc@1214 18 policy sendClient (SELECT fruit.Weight, fruit.Secret
adamc@1214 19 FROM fruit
adamc@1214 20 WHERE known(fruit.Secret))
adamc@1207 21
adamc@1214 22 policy sendClient (SELECT order.Id, order.Fruit, order.Qty
adamc@1214 23 FROM order, fruit
adamc@1214 24 WHERE order.Fruit = fruit.Id
adamc@1214 25 AND order.Qty = 13)
adamc@1200 26
adamc@1207 27 fun fname r =
adamc@1207 28 x <- queryX (SELECT fruit.Weight
adamc@1207 29 FROM fruit
adamc@1207 30 WHERE fruit.Nam = {[r.Nam]}
adamc@1210 31 AND fruit.Secret = {[r.Secret]}
adamc@1210 32 AND fruit.Weight <> 3.14
adamc@1210 33 AND fruit.Weight < 100.0
adamc@1210 34 AND fruit.Weight <= 200.1
adamc@1210 35 AND fruit.Weight > 1.23
adamc@1210 36 AND fruit.Weight >= 1.24)
adamc@1207 37 (fn r => <xml>Weight is {[r.Fruit.Weight]}</xml>);
adamc@1207 38
adamc@1207 39 return <xml><body>
adamc@1207 40 {x}
adamc@1207 41 </body></xml>
adamc@1207 42
adamc@1200 43 fun main () =
adamc@1204 44 x1 <- queryX (SELECT fruit.Id, fruit.Nam
adamc@1209 45 FROM fruit
adamc@1210 46 WHERE fruit.Nam = "apple")
adamc@1204 47 (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
adamc@1204 48
adamc@1204 49 x2 <- queryX (SELECT fruit.Nam, order.Qty
adamc@1204 50 FROM fruit, order
adamc@1206 51 WHERE fruit.Id = order.Fruit
adamc@1206 52 AND order.Qty = 13)
adamc@1204 53 (fn x => <xml><li>{[x.Fruit.Nam]}: {[x.Order.Qty]}</li></xml>);
adamc@1200 54
adamc@1228 55 ro <- oneOrNoRows (SELECT fruit.Id, fruit.Nam
adamc@1228 56 FROM fruit);
adamc@1228 57
adamc@1200 58 return <xml><body>
adamc@1204 59 <ul>{x1}</ul>
adamc@1210 60
adamc@1204 61 <ul>{x2}</ul>
adamc@1207 62
adamc@1228 63 {case ro of
adamc@1228 64 None => <xml>None</xml>
adamc@1228 65 | Some _ => <xml>Some</xml>}
adamc@1228 66
adamc@1207 67 <form>
adamc@1207 68 Fruit name: <textbox{#Nam}/><br/>
adamc@1207 69 Secret: <textbox{#Secret}/><br/>
adamc@1207 70 <submit action={fname}/>
adamc@1207 71 </form>
adamc@1200 72 </body></xml>