tests/course2.mlw

   1 module M
   2
   3   use int.Int
   4   use module stdlib.Ref
   5
   6   (* preliminaries *)
   7
   8   use array.Array as A
   9
  10   type array 'a = A.t int 'a
  11
  12   logic injective (n:int) (m:int) (a:array 'a) =
  13     forall i j:int. n <= i <= m -> n <= j <= m ->
  14        A.get a i = A.get a j -> i = j
  15
  16   type string
  17
  18   (* Capucine memory model *)
  19
  20   type pointer
  21
  22   type region 'a = A.t pointer 'a
  23
  24 (*
  25   type first_free_addr = int
  26
  27   logic valid (a:first_free_addr) (p:pointer) = p < a
  28
  29   logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
  30      forall i:int. n <= i <= m -> valid a (A.get r i)
  31
  32 parameter alloc : ref first_free_addr
  33
  34 parameter new_pointer : tt:unit ->
  35   { }
  36   pointer
  37   writes alloc
  38   { alloc = old alloc + 1 and result = old alloc }
  39 *)
  40
  41
  42 (*
  43 record Student =
  44   name: string;
  45   mark: int
  46   inv(this) { 0 <= this.mark <= 100 }
  47 end
  48 *)
  49
  50   type student = (string, int)
  51
  52   logic invStudent (this:student) =
  53      let (_,m) = this in 0 <= m <= 100
  54
  55 (*
  56 record Course =
  57   group Rstud: Student;
  58   students: array [Rstud]
  59   count: int
  60   sum: int
  61   inv(this) {
  62     count >= 0
  63     and
  64     injective(0, count-1, this.students)
  65     and
  66     this.sum = mark_sum(0,this.count-1,this.students)
  67   }
  68 end
  69 *)
  70
  71   type course = (region student, array pointer, int, int)
  72
  73 (* markSum(r,i,j,a) donne \sigma_{k=i,j} get(r,a[k]).mark *)
  74
  75   logic markSum (region student) int int (array pointer) : int
  76
  77 (* axiom MarkSumEmpty :
  78      forall region r:Student,
  79         forall i j:int, forall a:(array pointer),
  80         i > j -> markSum(r,i,j,a) = 0
  81 *)
  82
  83   axiom MarkSumEmpty :
  84     forall r:region student, i j:int, a : array pointer.
  85       i > j -> markSum r i j a = 0
  86
  87 (* axiom MarkSumNonEmpty :
  88      forall region r:Student,
  89         forall i j:int, forall a:(array [r]),
  90         i <= j ->
  91           let p = array_get a j in
  92           markSum(r,i,j,a) = markSum(r,i,j-1,a)  + get(r,p).mark
  93 *)
  94
  95   axiom MarkSumNonEmpty :
  96     forall r:region student, i j:int, a : array pointer.
  97       i <= j ->
  98         let p = A.get a j in
  99         let (_,mark) = A.get r p in
 100         markSum r i j a = markSum r i (j-1) a  + mark
 101
 102 (* a essayer mais pas essentiel
 103   logic markSum (r:region student) (i:int) (j:int) (a:array pointer) : int =
 104     if i > j then 0 else ...
 105 *)
 106
 107
 108 (*
 109   lemma MarkSumFootprint:
 110   forall n:int. forall s1: array(Student [R1]).
 111   forall s2: array(Student [R2]).
 112   (forall i:int. [0] <= [i] and [i] < [n] ==>
 113      [!(select(s1,i) : Student[R1]).mark] =
 114        [!(select(s2,i) : Student[R2]).mark])
 115   ==> [MarkSum(n, s1)] = [MarkSum(n,s2)]
 116 *)
 117
 118
 119 (*
 120   lemma MarkSum_set_array_outside :
 121      forall region r:Student. forall i j k:int, a: array [r], p:pointer.
 122      not (i <= k <= j) ->
 123      markSum(r,i,j,array_set(a,k,p)) = markSum(r,i,j,a)
 124
 125 *)
 126
 127   lemma MarkSum_set_array_outside :
 128      forall r:region student, i j k:int, a: array pointer, p:pointer.
 129      not (i <= k <= j) ->
 130      markSum r i j (A.set a k p) = markSum r i j a
 131
 132 (*
 133
 134   lemma MarkSum_set_region_outside :
 135      forall region r:Student. forall i j:int, a: array [r], p:pointer, s:student.
 136      (forall k:int. i <= k <= j -> A.get a k <> p) ->
 137      markSum (A.set r p s) i j a = markSum r i j a
 138 *)
 139
 140   lemma MarkSum_set_region_outside :
 141      forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
 142      (forall k:int. i <= k <= j -> A.get a k <> p) ->
 143      markSum (A.set r p s) i j a = markSum r i j a
 144
 145
 146
 147
 148   logic invCourse (alloc:first_free_addr) (this:course) =
 149      let (rStud,students,count,sum) = this in
 150      count >= 0
 151      and
 152      valid_array alloc 0 (count - 1) students
 153      and
 154      injective 0 (count - 1) students
 155      and
 156      sum = markSum rStud 0 (count-1) students
 157
 158 (*
 159 fun CreateCourse(R:[Course]): [R]
 160   consumes R^e
 161   produces R^c
 162 =
 163   let c = new Course [R] in
 164   c.count = 0;
 165   c.sum = 0;
 166   pack c;
 167   c
 168 *)
 169
 170 let createCourse (r: (ref (region course))) : pointer =
 171   { }
 172     let c = new_pointer () in
 173     let (rStud,student,count,sum) = A.get !r c in
 174     let newc = (rStud,student,0,0) in
 175     r := A.set !r c newc;
 176     assert { invCourse alloc newc };
 177     c
 178   { valid alloc result }
 179
 180 (*
 181 fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
 182   consumes R^c
 183   produces R^c
 184 =
 185   region S in
 186   let s = new Student[S] in
 187   s := (name, 0);
 188   assert forall i:int, array_get c.students i in rStud;
 189   (adoptregion S as R.R_s);
 190   " assume forall p:pointer. p in old(R.R_S) -> p <> s "
 191   assert [MarkSum(!(!c.students))] = [old(MarkSum(!(!c.students)))];
 192   (focus !c.students) := add(!(!c.students), s);
 193   c := (!c.students, !c.count + 1, !c.total, !c.4);
 194   s
 195 *)
 196
 197 let registerStudent
 198     (r: (ref (region course))) (c:pointer) (name:string) : pointer =
 199 { valid alloc c and invCourse alloc (A.get r c) }
 200   let s = new_pointer () in
 201   let (rStud,student,count,sum) = A.get !r c in
 202   let newstud = (name,0) in
 203   assume { forall p:pointer. in_region(p,old rStud) -> p <> s } ;
 204   let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
 205   r := A.set !r c newc;
 206   assert { invCourse alloc newc };
 207   s
 208 { valid alloc result }
 209
 210 (*
 211
 212 fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
 213   consumes R^c
 214   produces R^c
 215 {
 216   unpack c  (* c.Rstud^G, R^o *)
 217   let region Rs:Student
 218   let s' = focus s as Rs (* Rs -o c.Rstud, Rs^c, R^o *)
 219   unpack s' (* Rs -o c.Rstud, Rs^o, R^o *)
 220   s'.mark <- mark;
 221   pack s';
 222   pack c
 223 }
 224
 225 *)
 226
 227 end
 228
 229 (*
 230 Local Variables:
 231 compile-command: "unset LANG; make -C ../.. examples/programs/course"
 232 End:
 233 *)