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