RiSE4fun samples for ChaliceList of built-in samples for the Chalice in RiSE4funen-US<a target='_blank' href='https://go.microsoft.com/?linkid=2028325'>Contact Us</a>| <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=521839'>Privacy &amp; Cookies</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkID=246338'>Terms of Use</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=506942 '>Trademarks</a>| &copy; 2017 Microsofthttps://rise4fun.com//Images/Rise.gifRiSE4fun samples for Chalicehttps://rise4fun.com/Chalice/swapswap// This simple example has a method that swap the values of the F and G fields. // The method requires permission to both F and G, and it returns those // permissions along with the promise the F and G have swapped values. class C { var F: int; var G: int; method Swap() requires acc(F) && acc(G); ensures acc(F) && acc(G) && F == old(G) && G == old(F); { var tmp := F; F := G; G := tmp; } } https://rise4fun.com/Chalice/incinc// This example shows a method that increments the field y. // As stated in its specification, the method requires and returns // permission to y. The calling method (Main) obtains permission // to c.y when it allocates c, and can therefore call Inc(). Upon // return from Inc, Main checks that c.y has indeed been incremented // by 1, as the specification of Inc says will happen. // What happens if you remove one or more of the 3 specifications // of Inc? class Cell { var y: int; method Inc() requires acc(y); ensures acc(y); ensures y == old(y) + 1; { y := y + 1; } method Main() { var c := new Cell; c.y := 42; call c.Inc(); assert c.y == 43; } } https://rise4fun.com/Chalice/aliasingaliasing// This example shows that "acc" permissions are exclusive. That is, // the only way to have separate permissions to both c.y and d.y is // if c and d are references to different objects. The example also // shows what happens if a caller (Main) tries to call the method // with the same object twice. // Change Main to allocate another object and pass it as the second // parameter to TestAliasing. What happens if you then include the // assert that is commented out below? Why? class Cell { var y: int; method TestAliasing(c: Cell, d: Cell) requires acc(c.y) && acc(d.y); { assert c != d; } method Main() { var c := new Cell; call TestAliasing(c, c); // assert c.y == c.y; } } https://rise4fun.com/Chalice/OwickiGriesOwickiGries// This example shows the Owicki and Gries counter encoded in Chalice. // The Main method sets "counter" 0. It then forks 2 worker threads, // each of which will increment "counter" by 1. The specifications // allow Main to conclude that, after joining the worker threads, // "counter" is indeed 2. The specifications make use of ghost // variables "c0" and "c1", which essentially keep track of what each // worker thread does. Stability and access to the various variables // are accomplished by using fractional permissions, like the 50% // permission that is specified by "acc(c0,50)". // Try leaving out various parts of the specifications to see what // will happen. class OwickiGries { var counter: int ghost var c0: int ghost var c1: int invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1 method Main() { var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 } share og fork tk0 := og.Worker(false) fork tk1 := og.Worker(true) join tk0; join tk1 acquire og; unshare og assert og.counter == 2 } method Worker(b: bool) requires rd(mu) && waitlevel << mu requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50)) ensures rd(mu) ensures !b ==> acc(c0,50) && c0 == old(c0) + 1 ensures b ==> acc(c1,50) && c1 == old(c1) + 1 { lock (this) { counter := counter + 1 if (!b) { c0 := c0 + 1 } else { c1 := c1 + 1 } } } } https://rise4fun.com/Chalice/SieveSieve// This example shows a use of a channel. Properties of the messages // passed along the channel, as well as permissions and channel credits, // are specified in the channel's "where" clause. channel NumberStream(x: int) where 2 <= x ==> credit(this); class Sieve { method Counter(n: NumberStream, to: int) // sends the plurals along n requires rd(n.mu) && credit(n,-1) && 0 <= to; { var i := 2; while (i < to) invariant rd(n.mu); invariant 2 <= i; invariant credit(n, -1) { send n(i); i := i + 1; } send n(-1); } method Filter(prime: int, r: NumberStream, s: NumberStream) requires 2 <= prime; requires rd(r.mu) && waitlevel << r.mu; requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1); { receive x := r; while (2 <= x) invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu; invariant 2<= x ==> credit(r); invariant credit(s, -1); { if (x % prime != 0) { // suppress multiples of prime send s(x); } receive x := r; } send s(-1); } method Start() { var ch := new NumberStream; fork Counter(ch, 101); var p: int; receive p := ch; while (2 <= p) invariant ch != null; invariant 2 <= p ==> credit(ch, 1); invariant rd*(ch.mu) && waitlevel << ch.mu; { // print p--it's a prime! var cp := new ChalicePrint; call cp.Int(p); var n := new NumberStream between waitlevel and ch; fork Filter(p, ch, n); ch := n; receive p := ch; } } } external class ChalicePrint { method Int(x: int) { } }