why3/examples_in_progress/course.mlw

module Appmap

  use map.Map
  use map.Const

  type key

  type t 'a = abstract { contents: map key 'a }

  val function create (x: 'a): t 'a
    ensures { result.contents = const x }

  val function ([]) (m: t 'a) (k: key): 'a
    ensures { result = m.contents[k] }

  val function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
    ensures { result.contents = m.contents[k <- v] }

end

module M

  use int.Int
  use ref.Ref

  (* preliminaries *)

  clone Appmap with type key = int

  type array 'a = t 'a

  predicate injective (n:int) (m:int) (a:array 'a) =
    forall i j:int. n <= i <= m -> n <= j <= m ->
       a[i] = a[j] -> i = j

  type char_string

  (* Capucine memory model *)

  type pointer = int

  type region 'a = t 'a

  type first_free_addr = int

  predicate valid (a:first_free_addr) (p:pointer) = p < a

  predicate valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
     forall i:int. n <= i <= m -> valid a (r[i])

val alloc : ref first_free_addr

val new_pointer (_tt:unit) : pointer writes { alloc }
  ensures { !alloc = old !alloc + 1 /\ result = old !alloc }

(*
record Student =
  name: char_string;
  mark: int
  inv(this) { 0 <= this.mark <= 100 }
end
*)

  type student = (char_string, int)

  predicate 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
    /\
    injective(0, count-1, this.students)
    /\
    this.sum = mark_sum(0,this.count-1,this.students)
  }
end
*)

  type course = (region student, array pointer, int, int)

  function 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) = r[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] /\ [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[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[k] <> p) ->
     markSum (r[p <- s]) i j a = markSum r i j a




  predicate invCourse (alloc:first_free_addr) (this:course) =
     let (rStud,students,count,sum) = this in
     count >= 0
     /\
     valid_array alloc 0 (count - 1) students
     /\
     injective 0 (count - 1) students
     /\
     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
  ensures { valid !alloc result }
  = let c = new_pointer () in
    let (rStud,student,_count,_sum) = !r[c] in
    let newc = (rStud,student,0,0) in
    r := !r[c <- newc];
    assert { invCourse !alloc newc };
    c

(*
fun RegisterStudent(R:[Course], c: [R], name: char_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:char_string) : pointer
requires { valid !alloc c /\ invCourse !alloc !r[c] }
ensures  { valid !alloc result }
= let s = new_pointer () in
  let (rStud,student,count,sum) = !r[c] in
  let newstud = (name,0) in
  let newc = (rStud[s <- newstud],student[count <- s],count+1,sum) in
  r := !r[c <- newc];
  assert { invCourse !alloc newc };
  s

(*

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
}

*)

end