Capucine Example: Course and Students

This example is work in progress. To compile it, go into the capucine directory and type:
logic type set (A)
logic function empty(): set (A)
logic function cardinal(set (A)): int
logic function add(set (A), A): set (A)
predicate inset(x: A, s: set(A))

axiom NotInsetEmpty:
  forall x: A. not inset(x, empty)

axiom NotInsetAdd:
  forall x: A.
  forall s: set (A).
  forall y: A.
  x <> y ==> not inset(x, s) ==> not inset(x, [add(s, y)])

axiom InsetAdd:
  forall x: A.
  forall s: set (A).
  inset(x, [add(s, x)])

axiom InsetAdd:
  forall x: A.
  forall y: A.
  forall s: set (A).
  inset(x, s) ==> inset(x, [add(s, y)])

class Student =
  (int * int)
end

selector (name, mark)

class StudentCollection {R} =
  set (Student [R])
end

selector (students, minmark)

class Course =
  own R_s, R_c;
  (StudentCollection {R_s} [R_c]
   * int
   * Student [R_s]) (* HACK to solve a stupid problem, ignore this *)
  invariant (c) =
    forall s: Student [R_s].
      inset(s, [!(c.students)]) ==> [!s.mark] >= [c.minmark]
end

val CreateCourse(minmark: int): Course [R]
  consumes R^e
  produces R^c
  ensures [!result.minmark] = minmark
=
  region PLOP in
  let c = new Course [PLOP] in
  let students = new StudentCollection {PLOP.R_s} [PLOP.R_c] in
  students := empty;
  c := (students, minmark, new Student);
  c

val CreateStudent(c: Course [R], name: int, mark: int): Student [R.R_s]
  consumes R^c
  produces R^c
  ensures
    [!result.mark] = mark
    and inset(result, [!(!c.students)])
    and forall s: Student [R.R_s].
      inset(s, [old(!(!c.students))]) ==>
      inset(s, [!(!c.students)])
=
  let s = new Student in
  s := (name, mark);
  (focus !c.students) := add(!(!c.students), s);
  let min =
    let current = !c.minmark in
    if mark < current then mark else current
  in
  c := (!c.students, min, !c.3);
  s

val SetMark(c: Course [R], s: Student [R.R_s], mark: int): unit
  consumes R^c
  produces R^c
  ensures [!s.mark] = mark and [!c.students] = [old(!c.students)]
=
  let min =
    let current = !c.minmark in
    if mark < current then mark else current
  in
  c := (!c.students, min, !c.3);
  (focus s) := (!s.name, mark)

val MinMark(c: Course [R]): int
  consumes R^c
  produces R^c
  ensures result = [!c.minmark]
=
  !c.minmark

val main(): unit
=
  region ALGEBRA: Course in
  region TOPOLOGY: Course in
  let algebra = (CreateCourse(100): Course [ALGEBRA]) in
  let alice = CreateStudent(algebra, 1, 80) in
  let bob = CreateStudent(algebra, 2, 30) in
  SetMark(algebra, alice, 70);
  SetMark(algebra, bob, 50);
  let topology = (CreateCourse(100): Course [TOPOLOGY]) in
  let charlie = CreateStudent(topology, 3, 20) in
  SetMark(topology, charlie, 90);
  let m = MinMark(algebra) in
  assert (m <= [!alice.mark] and (m <= [!bob.mark]))
Capucine Example: Course and Students

Discussion

Code
