{

  (* preliminaries *)

  use array.Array as A

  type array 'a = A.t int 'a

  logic injective (n:int) (m:int) (a:array 'a) =
    forall i j:int. n <= i <= m -> n <= j <= m ->
       A.get a i = A.get a j -> i = j

  type string

  (* Capucine memory model *)

  type pointer = int

  type region 'a = A.t pointer 'a

  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) =
     forall i:int. n <= i <= m -> valid a (A.get r i)

}

parameter alloc : ref first_free_addr

parameter new_pointer : tt:unit ->
  { }
  pointer
  writes alloc
  { !alloc = old !alloc + 1 and result = old !alloc }

(*
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 ->
        let (_,mark) = A.get r (A.get a j) in
        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) ->
     markSum r i j (A.set a k p) = markSum r i j a


  lemma MarkSum_set_region_outside :
     forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
     (forall k:int. i <= k <= j -> A.get a k <> p) ->
     markSum (A.set r p s) i j a = markSum r i j a




  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
    let (rStud,student,count,sum) = A.get !r c in
    let newc = (rStud,student,0,0) in
    r := A.set !r c newc;
    assert { invCourse !alloc newc };
    c
  { valid !alloc result }

(*
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 =
{ valid !alloc c and invCourse !alloc (A.get !r c) }
  let s = new_pointer () in
  let (rStud,student,count,sum) = A.get !r c in
  let newstud = (name,0) in
  let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
  r := A.set !r c newc;
  assert { invCourse !alloc newc };
  s
{ valid !alloc result }

(*

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
}

*)