examples_in_progress/course.mlw

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