Capucine Example: Course and Students

make examples/course.gwhy

type array ('a)

logic empty_array (): array ('a)

logic store (a: array ('a), i: int, v: 'a): array ('a)

logic select (a: array ('a), i: int): 'a

axiom select_eq:
  forall a: array ('a).
  forall i: int.
  forall v: 'a.
  select(store(a, i, v), i) = v

axiom select_neq:
  forall a: array ('a).
  forall i: int.
  forall j: int.
  forall v: 'a.
  i <> j ==>
  select(store(a, i, v), j) = select(a, j)

(*****************************************************************************)

class Student
{
  mark: int;
}

(* sum between i and j-1 *)
(* If marksum is always from 0, provers actually have much more difficulty
   proving stuff! (I checked that they would not prove false...) *)
logic mark_sum [Rs: Student] (a: array ([Rs]), i: int, j: int): int

axiom MSempty:
  forall region Rs: Student.
  forall a: array ([?]).
  forall i: int.
  mark_sum [Rs] (a, i, i) = 0

axiom MSsingleton:
  forall region Rs: Student.
  forall a: array ([?]).
  forall i: int.
  mark_sum [Rs] (a, i, i+1) = get(Rs, select(a, i), mark)

axiom MSsplit:
  forall region Rs: Student.
  forall a: array ([?]).
  forall i: int.
  forall j: int.
  forall k: int.
  i <= k && k <= j ==>
  mark_sum [Rs] (a, i, j) = mark_sum [Rs] (a, i, k) + mark_sum [Rs] (a, k, j)

axiom MSfootprint:
  forall region Rold: Student.
  forall region Rnew: Student.
  forall Aold: array ([?]).
  forall Anew: array ([?]).
  forall left: int.
  forall right: int.
  (forall i: int. left <= i && i < right ==>
     get (Rold, select(Aold, i), mark) =
     get (Rnew, select(Anew, i), mark)) ==>
  mark_sum [Rold] (Aold, left, right) = mark_sum [Rnew] (Anew, left, right)

class Course
{
  group Rstudents: Student;
  students: array ([Rstudents]);
  sum: int;
  count: int;
  invariant
    sum = mark_sum [Rstudents] (students, 0, count) &&
    count >= 0 &&
    (forall i: int. forall j: int.
     0 <= i && i < count ==>
     0 <= j && j < count ==>
     i <> j ==>
     select(students, i) <> select(students, j)) &&
    (forall p: [?]. p in Rstudents ==>
     exists i: int. 0 <= i && i < count && p = select(students, i))
}

fun create_course [R: Course] (): [R]
  consumes R^e
  produces R^c
  post get(R, result, count) = 0
{
  let c = new [R];
  c.students <- #empty_array ();
  c.sum <- 0;
  c.count <- 0;
  return c
}

fun add_student [Rc: Course] (c: [Rc], m: int): [c.Rstudents]
  consumes Rc^c
  produces Rc^c
  post
    get(get(Rc, c, Rstudents), result, mark) = m &&
    get(Rc, c, count) = get(Rc, c, count)@pre + 1 &&
    get(Rc, c, sum) = get(Rc, c, sum)@pre + m &&

    forall s: [?]. s in get(Rc, c, Rstudents)@pre ==>
    get(get(Rc, c, Rstudents), s, mark) =
    get(get(Rc, c, Rstudents), s, mark)@pre
{
  use invariant c;
  let region Rs: Student;
  let s = new [Rs];
  s.mark <- m;

  use
    forall i: int. i >= 0 && i < get(Rc, c, count) ==>
    select(get(Rc, c, students), i) <> s;

  adopt Rs as c.Rstudents;
  c.students <- #store (c.students, c.count, s);
  c.sum <- c.sum + m;
  c.count <- c.count + 1;

  return s
}

fun change_mark [Rc: Course] (c: [Rc], s: [c.Rstudents], m: int): unit
  consumes Rc^c
  produces Rc^c
  post
    get(get(Rc, c, Rstudents), s, mark) = m &&
    get(Rc, c, sum) = get(Rc, c, sum)@pre + m -
      get(get(Rc, c, Rstudents), s, mark)@pre &&
    get(Rc, c, count) = get(Rc, c, count)@pre &&

    forall i: int.
    0 <= i && i < get(Rc, c, count) ==>
    s <> select(get(Rc, c, students), i) ==>
    get(get(Rc, c, Rstudents), select(get(Rc, c, students), i), mark) =
    get(get(Rc, c, Rstudents), select(get(Rc, c, students), i), mark)@pre
{
  use invariant c;
  use s in get(Rc, c, Rstudents);

  label before;
  let region F: Student;
  focus s as F;
  c.sum <- c.sum - s.mark + m;
  s.mark <- m;
  unfocus F as c.Rstudents;

  (* Helps Z3 mono to prove the invariant of c *)
  assert
    exists i: int.
      0 <= i && i < get(Rc, c, count) &&
      select(get(Rc, c, students), i) = s &&
    mark_sum [get(Rc, c, Rstudents)] (get(Rc, c, students), 0, i) =
      mark_sum [get(Rc, c, Rstudents)] (get(Rc, c, students), 0, i)@before &&
    mark_sum [get(Rc, c, Rstudents)]
      (get(Rc, c, students), i+1, get(Rc, c, count)) =
      mark_sum [get(Rc, c, Rstudents)]
        (get(Rc, c, students), i+1, get(Rc, c, count))@before;
}

fun main (x: unit): unit
{
  let region Ra: Course;
  let algebra = create_course [Ra] ();

  let region Rb: Course;
  let physics = create_course [Rb] ();

  use invariant algebra;

  assert get(Ra, algebra, count) = 0;
  assert get(Ra, algebra, sum) = 0;

  let anna = add_student [Ra] (algebra, 10);

  (* pour utiliser l'invariant de algebra *)
  use anna in get(Ra, algebra, Rstudents);

  assert get(get(Ra, algebra, Rstudents), anna, mark) = 10;

  use invariant algebra;

  assert get(Ra, algebra, count) = 1;
  assert get(Ra, algebra, sum) = 10;

  let elisa = add_student [Ra] (algebra, 20);

  assert get(get(Ra, algebra, Rstudents), anna, mark) = 10;

  use invariant algebra;

  assert get(Ra, algebra, count) = 2;
  assert get(Ra, algebra, sum) = 30;

  use invariant physics;

  assert get(Rb, physics, count) = 0;
  assert get(Rb, physics, sum) = 0;

  let carolina = add_student [Rb] (physics, 7);

  use invariant physics;

  assert get(Ra, algebra, count) = 2;
  assert get(Ra, algebra, sum) = 30;

  assert get(Rb, physics, count) = 1;
  assert get(Rb, physics, sum) = 7;

  assert get(get(Ra, algebra, Rstudents), elisa, mark) = 20;

  let x = change_mark [Ra] (algebra, anna, 18);
  assert get(get(Ra, algebra, Rstudents), anna, mark) = 18;

  assert get(get(Ra, algebra, Rstudents), elisa, mark) = 20;

  use invariant algebra;

  assert get(Ra, algebra, count) = 2;
  assert get(Ra, algebra, sum) = 38;

  assert get(Rb, physics, count) = 1;
  assert get(Rb, physics, sum) = 7;
}