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/GroupeClassement.java
 *)
module GroupeClassement
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]

  use int.Int
  use seq.Seq
  use seq.Distinct

  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.lang.Integer
  use mach.java.util.List
  use mach.java.util.Set
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.exceptions.invalid_argument_exception.InvalidArgumentException
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  type t [@java:visibility:package] = {
    c_gp_cod : integer;
    taux_min_boursiers_pourcents : integer;
    taux_min_du_secteur_pourcents : integer;
    voeux_classes : list VoeuClasse.t;
  }

  let groupe_classement [@java:constructor]
      (c_gp_cod : integer)
      (taux_min_boursiers_pourcents : integer)
      (taux_min_du_secteur_pourcents : integer)
      : t
    ensures { result.c_gp_cod = c_gp_cod }
    ensures { result.taux_min_boursiers_pourcents = taux_min_boursiers_pourcents }
    ensures { result.taux_min_du_secteur_pourcents = taux_min_du_secteur_pourcents }
    ensures { List.size result.voeux_classes = 0 }
  =
    {
      c_gp_cod = c_gp_cod;
      taux_min_boursiers_pourcents = taux_min_boursiers_pourcents;
      taux_min_du_secteur_pourcents = taux_min_du_secteur_pourcents;
      voeux_classes = List.empty ();
    }

  let ghost function seq_voeux_classes[@java:ignore] (self : t) : Seq.seq VoeuClasse.t
    ensures { result = self.voeux_classes }
  =
    List.content self.voeux_classes

  meta coercion function seq_voeux_classes

  let function get_c_gp_cod (self : t) : integer
  =
    self.c_gp_cod

  let function get_nb_voeux_classes (self : t) : integer
  =
    List.size self.voeux_classes

  let function get_voeux_classes (self : t) : list VoeuClasse.t
  =
    self.voeux_classes

  let get_ith_voeu_classe_safe [@java:visibility:package] (self : t) (i : integer) : VoeuClasse.t
    requires { 0 <= i < get_nb_voeux_classes self }
    ensures { result = self[i] }
  =
    try
      List.get self.voeux_classes i
    with
      | IndexOutOfBoundsException.E _ -> absurd
    end

  let function get_taux_min_boursiers_pourcents (self :t) : integer
  =
    self.taux_min_boursiers_pourcents

  let function get_taux_min_du_secteur_pourcents (self :t) : integer
  =
    self.taux_min_du_secteur_pourcents

  let add (self : t) (v : VoeuClasse.t): unit
    raises { VerificationException.E _ -> get_nb_voeux_classes self >= max_integer }
  =
    if get_nb_voeux_classes self >= max_integer then
      raise VerificationException.E (crtX0 GROUPE_CLASSEMENT_POSSIBLE_DEPASSEMENT_ARITHMETIQUE);
    let _ = List.add self.voeux_classes v in ()

  clone export fr.parcoursup.whyml.ordreappel.algo.groupe_classement_clone.GroupeClassementClone with type t = t,
    val get_c_gp_cod = get_c_gp_cod,
    val get_nb_voeux_classes = get_nb_voeux_classes,
    val get_ith_voeu_classe_safe = get_ith_voeu_classe_safe,
    val get_taux_min_boursiers_pourcents = get_taux_min_boursiers_pourcents,
    val get_taux_min_du_secteur_pourcents = get_taux_min_du_secteur_pourcents,
    val seq_voeux_classes = seq_voeux_classes

  let verifier_coherence_taux [@java:visibility:private] (self : t) : unit
    ensures { 0 <= get_taux_min_boursiers_pourcents self <= 100 }
    ensures { 0 <= get_taux_min_du_secteur_pourcents self <= 100 }
    raises { VerificationException.E _ -> not (0 <= get_taux_min_boursiers_pourcents self <= 100 &&
                                               0 <= get_taux_min_du_secteur_pourcents self <= 100) }
  =
    let tx_b : integer = get_taux_min_boursiers_pourcents self in
    if tx_b < 0 || tx_b > 100 then
      raise VerificationException.E (crtX1 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_TAUX_BOURSIER tx_b);
    let tx_r : integer = get_taux_min_du_secteur_pourcents self in
    if tx_r < 0 || tx_r > 100 then
      raise VerificationException.E (crtX1 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_TAUX_HORS_SECTEUR tx_r)

  let verifier_rangs [@java:visibility:private] (self : t) : unit
    requires { get_nb_voeux_classes self < Integer.max_integer }
    ensures { seq_rangs_uniques self }
    ensures { seq_rangs_ge_1 self }
    ensures { seq_distinct self }
    raises { VerificationException.E _ -> not (seq_rangs_uniques self && seq_rangs_ge_1 self) }
  =
    let rangs : set integer = Set.empty () in
    let nb_voeux : integer = get_nb_voeux_classes self in
    for i = 0 to nb_voeux - 1 do
      invariant { Set.size rangs = i }
      invariant { [@expl:rg>=1] seq_rangs_ge_1_loc self i }
      invariant { field_in_set self rangs get_rang i }
      invariant { set_in_field self rangs get_rang i }
      invariant { [@expl:rg unique] seq_field_uniques_loc self get_rang i }

      let rg = get_ith_rang_safe self i in

      if rg <= 0 then
        raise VerificationException.E (crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_RANG_NEGATIF
                                         (get_ith_g_cn_cod_safe self i) rg);

      if not Set.add rangs rg then
        raise VerificationException.E (crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_DUPLICATION_RANG
                                         (get_ith_g_cn_cod_safe self i) rg);
    done

  let verifier_rangs_appel [@java:visibility:private] (self : t) : unit
    requires { get_nb_voeux_classes self < Integer.max_integer }
    ensures { seq_rangs_appel_uniques self }
    ensures { seq_rangs_appel_ge_1 self }
    raises { VerificationException.E _ -> not (seq_rangs_appel_uniques self && seq_rangs_appel_ge_1 self) }
  =
    let rangs : set integer = Set.empty () in
    let nb_voeux : integer = get_nb_voeux_classes self in
    for i = 0 to nb_voeux - 1 do
      invariant { Set.size rangs = i }
      invariant { [@expl:rg>=1] seq_rangs_appel_ge_1_loc self i }
      invariant { field_in_set self rangs get_rang_appel i }
      invariant { set_in_field self rangs get_rang_appel i }
      invariant { [@expl:rg unique] seq_field_uniques_loc self get_rang_appel i }

      let rg = get_ith_rang_appel_safe self i in

      if rg <= 0 then
        raise VerificationException.E (crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_RANG_APPEL_NEGATIF
                                         (get_ith_g_cn_cod_safe self i) rg);

      if not Set.add rangs rg then
        raise VerificationException.E (crtX2 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_DUPLICATION_RANG_APPEL
                                         (get_ith_g_cn_cod_safe self i) rg);
    done

  let verifier_g_cn_cod [@java:visibility:private] (self : t) : unit
    requires { get_nb_voeux_classes self < Integer.max_integer }
    ensures { seq_g_cn_cod_ge_0 self }
    ensures { seq_g_cn_cod_uniques self }
    raises { VerificationException.E _ -> not (seq_g_cn_cod_ge_0 self /\ seq_g_cn_cod_uniques self) }
  =
    let cn_cods : set integer = Set.empty () in
    let nb_voeux : integer = get_nb_voeux_classes self in
    for i = 0 to nb_voeux - 1 do
      invariant { Set.size cn_cods = i }
      invariant { [@expl:g_cn_cod >=0 ] seq_g_cn_cod_ge_0_loc self i }
      invariant { field_in_set self cn_cods get_g_cn_cod i }
      invariant { set_in_field self cn_cods get_g_cn_cod i }
      invariant { [@expl:g_cn_cod unique] seq_field_uniques_loc self get_g_cn_cod i }

      let g_cn_cod = get_ith_g_cn_cod_safe self i in

      if g_cn_cod < 0 then
        raise VerificationException.E (crtX2 GROUPE_CLASSEMENT_GCNCOD_NEGATIF g_cn_cod (get_c_gp_cod self));

      if not Set.add cn_cods g_cn_cod then
        raise VerificationException.E (crtX1 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_GCNCOD_DUPLIQUE g_cn_cod);
    done

  let verifier_rangs_tries [@java:visibility:private] (self : t) : unit
    requires { get_nb_voeux_classes self < Integer.max_integer }
    requires { seq_rangs_uniques self }
    requires { seq_rangs_ge_1 self }
    ensures { seq_rangs_sorted self }
    raises { VerificationException.E _ -> not (seq_rangs_sorted self) }
  =
    let nb_voeux : integer = get_nb_voeux_classes self in
    for i = 0 to nb_voeux - 1 do
      invariant { seq_rangs_sorted_loc self i}

      if i = 0 || get_ith_rang_safe self (i - (1:integer)) < get_ith_rang_safe self i then
        continue;
      raise VerificationException.E (crtX1 GROUPE_CLASSEMENT_RANGS_NON_TRIES (get_c_gp_cod self));
    done

  let verifier_groupe_ok (self : t) : unit
    ensures { groupe_ok self }
    raises { VerificationException.E _ -> not (groupe_ok self) }
  =
    if get_nb_voeux_classes self > Integer.max_integer - 1 then
      raise VerificationException.E (crtX0 GROUPE_CLASSEMENT_POSSIBLE_DEPASSEMENT_ARITHMETIQUE);
    verifier_coherence_taux self;
    verifier_rangs self;
    verifier_rangs_appel self;
    verifier_g_cn_cod self

  let verifier_groupe_valid (self : t) : unit
    ensures { groupe_ok self }
    ensures { seq_rangs_sorted self }
    raises { VerificationException.E _ -> not (groupe_ok self && seq_rangs_sorted self) }
  =
    verifier_groupe_ok self;
    verifier_rangs_tries self
end

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

Generated by why3doc 1.7.2+git