course.mlw 4.12 KB
 Jean-Christophe Filliâtre committed Dec 29, 2010 1 ``````module M `````` MARCHE Claude committed Dec 14, 2010 2 `````` `````` Jean-Christophe Filliâtre committed Dec 30, 2010 3 `````` use import int.Int `````` Jean-Christophe Filliâtre committed May 16, 2011 4 `````` use import module ref.Ref `````` MARCHE Claude committed Jan 21, 2011 5 `````` `````` MARCHE Claude committed Dec 14, 2010 6 7 `````` (* preliminaries *) `````` Jean-Christophe Filliâtre committed May 13, 2011 8 `````` use map.Map as M `````` MARCHE Claude committed Dec 14, 2010 9 `````` `````` Jean-Christophe Filliâtre committed May 13, 2011 10 `````` type array 'a = M.map int 'a `````` MARCHE Claude committed Dec 14, 2010 11 12 13 `````` logic injective (n:int) (m:int) (a:array 'a) = forall i j:int. n <= i <= m -> n <= j <= m -> `````` Jean-Christophe Filliâtre committed May 13, 2011 14 `````` M.get a i = M.get a j -> i = j `````` MARCHE Claude committed Dec 14, 2010 15 16 17 18 19 20 21 `````` type string (* Capucine memory model *) type pointer = int `````` Jean-Christophe Filliâtre committed May 13, 2011 22 `````` type region 'a = M.map pointer 'a `````` MARCHE Claude committed Dec 14, 2010 23 24 25 26 27 28 `````` type first_free_addr = int logic valid (a:first_free_addr) (p:pointer) = p < a logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) = `````` Jean-Christophe Filliâtre committed May 13, 2011 29 `````` forall i:int. n <= i <= m -> valid a (M.get r i) `````` MARCHE Claude committed Dec 14, 2010 30 31 32 33 34 35 36 `````` parameter alloc : ref first_free_addr parameter new_pointer : tt:unit -> { } pointer writes alloc `````` Jean-Christophe Filliâtre committed May 20, 2011 37 `````` { !alloc = old !alloc + 1 and result = old !alloc } `````` MARCHE Claude committed Dec 14, 2010 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 `````` (* record Student = name: string; mark: int inv(this) { 0 <= this.mark <= 100 } end *) type student = (string, int) logic invStudent (this:student) = let (_,m) = this in 0 <= m <= 100 (* record Course = group Rstud: Student; students: array [Rstud] count: int sum: int inv(this) { count >= 0 and injective(0, count-1, this.students) and this.sum = mark_sum(0,this.count-1,this.students) } end *) type course = (region student, array pointer, int, int) logic markSum (region student) int int (array pointer) : int axiom MarkSumEmpty : forall r:region student, i j:int, a : array pointer. i > j -> markSum r i j a = 0 axiom MarkSumNonEmpty : forall r:region student, i j:int, a : array pointer. i <= j -> `````` Jean-Christophe Filliâtre committed May 13, 2011 79 `````` let (_,mark) = M.get r (M.get a j) in `````` MARCHE Claude committed Dec 14, 2010 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 `````` markSum r i j a = markSum r i (j-1) a + mark (* lemma MarkSumFootprint: forall n:int. forall s1: array(Student [R1]). forall s2: array(Student [R2]). (forall i:int. [0] <= [i] and [i] < [n] ==> [!(select(s1,i) : Student[R1]).mark] = [!(select(s2,i) : Student[R2]).mark]) ==> [MarkSum(n, s1)] = [MarkSum(n,s2)] *) lemma MarkSum_set_array_outside : forall r:region student, i j k:int, a: array pointer, p:pointer. not (i <= k <= j) -> `````` Jean-Christophe Filliâtre committed May 13, 2011 95 `````` markSum r i j (M.set a k p) = markSum r i j a `````` MARCHE Claude committed Dec 14, 2010 96 97 98 99 `````` lemma MarkSum_set_region_outside : forall r:region student, i j:int, a: array pointer, p:pointer, s:student. `````` Jean-Christophe Filliâtre committed May 13, 2011 100 101 `````` (forall k:int. i <= k <= j -> M.get a k <> p) -> markSum (M.set r p s) i j a = markSum r i j a `````` MARCHE Claude committed Dec 14, 2010 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 `````` logic invCourse (alloc:first_free_addr) (this:course) = let (rStud,students,count,sum) = this in count >= 0 and valid_array alloc 0 (count - 1) students and injective 0 (count - 1) students and sum = markSum rStud 0 (count-1) students (* fun CreateCourse(R:[Course]): [R] consumes R^e produces R^c = let c = new Course [R] in c.count = 0; c.sum = 0; pack c; c *) let createCourse (r: (ref (region course))) : pointer = { } let c = new_pointer () in `````` Jean-Christophe Filliâtre committed May 13, 2011 131 `````` let (rStud,student,count,sum) = M.get !r c in `````` MARCHE Claude committed Dec 14, 2010 132 `````` let newc = (rStud,student,0,0) in `````` Jean-Christophe Filliâtre committed May 13, 2011 133 `````` r := M.set !r c newc; `````` Jean-Christophe Filliâtre committed May 20, 2011 134 `````` assert { invCourse !alloc newc }; `````` MARCHE Claude committed Dec 14, 2010 135 `````` c `````` Jean-Christophe Filliâtre committed May 20, 2011 136 `````` { valid !alloc result } `````` MARCHE Claude committed Dec 14, 2010 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 `````` (* fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud] consumes R^c produces R^c = region S in let s = new Student[S] in s := (name, 0); (adoptregion S as R.R_s); assert [MarkSum(!(!c.students))] = [old(MarkSum(!(!c.students)))]; (focus !c.students) := add(!(!c.students), s); c := (!c.students, !c.count + 1, !c.total, !c.4); s *) let registerStudent (r: (ref (region course))) (c:pointer) (name:string) : pointer = `````` Jean-Christophe Filliâtre committed May 20, 2011 155 ``````{ valid !alloc c and invCourse !alloc (M.get !r c) } `````` MARCHE Claude committed Dec 14, 2010 156 `````` let s = new_pointer () in `````` Jean-Christophe Filliâtre committed May 13, 2011 157 `````` let (rStud,student,count,sum) = M.get !r c in `````` MARCHE Claude committed Dec 14, 2010 158 `````` let newstud = (name,0) in `````` Jean-Christophe Filliâtre committed May 13, 2011 159 160 `````` let newc = (M.set rStud s newstud,M.set student count s,count+1,sum) in r := M.set !r c newc; `````` Jean-Christophe Filliâtre committed May 20, 2011 161 `````` assert { invCourse !alloc newc }; `````` MARCHE Claude committed Dec 14, 2010 162 `````` s `````` Jean-Christophe Filliâtre committed May 20, 2011 163 ``````{ valid !alloc result } `````` MARCHE Claude committed Dec 14, 2010 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 `````` (* fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit consumes R^c produces R^c { unpack c (* c.Rstud^G, R^o *) let region Rs:Student let s' = focus s as Rs (* Rs -o c.Rstud, Rs^c, R^o *) unpack s' (* Rs -o c.Rstud, Rs^o, R^o *) s'.mark <- mark; pack s'; pack c } *) `````` Jean-Christophe Filliâtre committed Dec 29, 2010 182 ``````end `````` MARCHE Claude committed Dec 14, 2010 183 `````` `````` Jean-Christophe Filliâtre committed Dec 30, 2010 184 185 186 187 188 ``````(* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/course" End: *)``````