Parcoursup / Calcul de l'ordre d'appel des candidats index


(*
 https://framagit.org/parcoursup/algorithmes-de-parcoursup/-/tree/master/src/main/java/fr/parcoursup/algos/ordreappel/algo/OrdreAppel.java
 *)
module OrdreAppel
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]

  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use mach.java.util.List
  use mach.java.util.UnmodifiableList as UL
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use fr.parcoursup.whyml.ordreappel.algo.candidat_classe.CandidatClasse as CC
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse as VC
  use fr.parcoursup.whyml.exceptions.invalid_argument_exception.InvalidArgumentException

  type t [@extraction:preserve_single_field] = {
     candidats : UL.ulist CC.t;
  } invariant { [@expl:rang_appel tries]
    forall i j. 0 <= i < j < Seq.length candidats
      -> CC.get_rang_appel candidats[i] < CC.get_rang_appel candidats[j]
  } invariant { [@expl:g_cn_cod unique]
    forall i j. 0 <= i < Seq.length candidats -> 0 <= j < Seq.length candidats ->
      i <> j -> CC.get_g_cn_cod candidats[i] <> CC.get_g_cn_cod candidats[j]
  } invariant { [@expl:g_cn_cod >= 0]
    forall i. 0 <= i < Seq.length candidats -> CC.get_g_cn_cod candidats[i] >= 0
  } invariant { [@expl:rang appel >= 0]
    forall i. 0 <= i < Seq.length candidats -> CC.get_rang_appel candidats[i] >= 0
  } invariant { [@expl:|oa| <= max_integer]
    Seq.length candidats <= Integer.max_integer
  } by {
    candidats = UL.empty ();
  }

  meta coercion function candidats

  let function get_nb_candidats (self : t) : integer
    ensures { result = Seq.length self }
  =
    UL.size self.candidats

  let get_ith_candidat_classe (self : t) (i : integer) : CC.t
    ensures { result = self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) }
  =
    if (not (0 <= i && i < get_nb_candidats self)) then
      raise InvalidArgumentException.E (index_out_of_bounds i);
    try
      UL.get self.candidats i
    with
      IndexOutOfBoundsException.E _ -> absurd
    end

  let get_ith_g_cn_cod (self : t) (i : integer) : integer
    ensures { result = CC.get_g_cn_cod self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) }
  =
    CC.get_g_cn_cod (get_ith_candidat_classe self i)

  let get_ith_rang_appel (self : t) (i : integer) : integer
    ensures { result = CC.get_rang_appel self[i] }
    raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) }
  =
    CC.get_rang_appel (get_ith_candidat_classe self i)

  let function ordre_appel [@java:constructor] [@java:visibility:package] (voeux : UL.ulist VC.t) : t
    requires { [@expl:pre |voeux| <= max_integer] UL.size voeux <= Integer.max_integer }
    requires { [@expl:pre c_gn_cod >= 0] seq_g_cn_cod_ge_0 voeux }
    requires { [@expl:pre rang_appel >= 1] seq_rangs_appel_ge_1 voeux }
    requires { [@expl:pre g_cn_cod unique] seq_g_cn_cod_uniques voeux }
    requires { [@expl:pre rang_appel ordonnes] seq_rangs_appel_sorted voeux }

    ensures { [@expl:|res|=|voeux|] get_nb_candidats result = UL.size voeux }
    ensures { [@expl:rang_appel tries]
      forall i j. 0 <= i < j < UL.size result.candidats -> CC.get_rang_appel result[i] < CC.get_rang_appel result[j] }
    ensures { [@expl:res eq input]
      forall i. 0 <= i < UL.size voeux -> CC.est_voeu_classe result[i] voeux[i] }
    ensures { [@expl: g_cn_cod unique]
      forall i j. 0 <= i < UL.size voeux -> 0 <= j < UL.size voeux ->
        i <> j -> CC.get_g_cn_cod result[i] <> CC.get_g_cn_cod result[j] }
  =
    try
      let lvc : list CC.t = List.empty () in
      let len = UL.size voeux in
      for i = 0 to len - 1 do
          invariant { Seq.length lvc = i }
          invariant { forall j. 0 <= j < i -> CC.get_rang_appel lvc[j] = VC.get_rang_appel voeux[j] }
          invariant { forall j. 0 <= j < i -> CC.get_g_cn_cod lvc[j] = VC.get_g_cn_cod voeux[j] }
          invariant { forall k l. 0 <= k < i -> 0 <= l < i -> k <> l -> CC.get_rang_appel lvc[k] <> CC.get_rang_appel lvc[l] }
          invariant { forall k l. 0 <= k < i -> 0 <= l < i -> k <> l -> CC.get_g_cn_cod lvc[k] <> CC.get_g_cn_cod lvc[l] }
          let vc = UL.get voeux i in
          let cc = CC.candidat_classe (VC.get_g_cn_cod vc) (VC.get_rang_appel vc) in
          let _ = List.add lvc cc in ();
      done;
      { candidats = List.copy_of lvc; }
    with
      IndexOutOfBoundsException.E _ -> absurd
    end
end

(* generated on Thu Jan 30 02:06:23 UTC 2025 from rev:  *)

Generated by why3doc 1.7.2+git