Parcoursup / Calcul de l'ordre d'appel des candidats index
module VerificationsResultatsAlgoOrdreAppel [@java:package:fr.parcoursup.whyml.verification] use int.Int use seq.Seq use mach.java.lang.Integer use mach.java.lang.IndexOutOfBoundsException use mach.java.util.List use mach.java.util.Map use mach.java.util.Set use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe use proofs.ordre_appel.rv_specs.RuntimeVerificationSpec as RVSpec use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_entree.AlgoOrdreAppelEntree as AOAE use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_sortie.AlgoOrdreAppelSortie as AOAS 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 use fr.parcoursup.whyml.verification.verification_resultats_algo_ordre_appel_p1.VerificationResultatsAlgoOrdreAppelP1 as VerifP1 use fr.parcoursup.whyml.verification.verification_resultats_algo_ordre_appel_p2.VerificationResultatsAlgoOrdreAppelP2 as VerifP2 use fr.parcoursup.whyml.verification.verification_resultats_algo_ordre_appel_p3.VerificationResultatsAlgoOrdreAppelP3 as VerifP3 use fr.parcoursup.whyml.verification.verification_resultats_algo_ordre_appel_p4.VerificationResultatsAlgoOrdreAppelP4 as VerifP4 use fr.parcoursup.whyml.verification.verification_resultats_algo_ordre_appel_p5.VerificationResultatsAlgoOrdreAppelP5 as VerifP5 let verifier_rangs_appel [@java:visibility:private] (grp : GroupeClassementValide.t) : unit ensures { seq_rangs_appel_ge_1 grp } ensures { seq_rangs_appel_uniques grp } raises { VerificationException.E _ -> not (seq_rangs_appel_ge_1 grp /\ seq_rangs_appel_uniques grp) } = let rangs : set integer = Set.empty () in let nb_voeux : integer = get_nb_voeux_classes grp in try begin for i = 0 to nb_voeux - 1 do invariant { [@expl:rg>=1] seq_rangs_appel_ge_1_loc grp i } invariant { field_in_set grp rangs get_rang_appel i } invariant { set_in_field grp rangs get_rang_appel i } invariant { [@expl:rg appel unique] seq_rangs_appel_uniques_loc grp i } invariant { Set.size rangs = i } let rg = get_ith_rang_appel grp i in if rg <= 0 then raise VerificationException.E (crtX0 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_INCONSISTENCE_DONNEES); if not Set.add rangs rg then raise VerificationException.E (crtX0 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_INCONSISTENCE_DONNEES); done end with | InvalidArgumentException.E _ -> absurd end let verifier_coherence_donnees_entree_sortie (grp_e : GroupeClassementValide.t ) (grp_s : GroupeClassementValide.t) requires { groupe_ok grp_e } requires { groupe_ok grp_s } ensures { RVSpec.grp_eq_up_to_rang_appel grp_e grp_s } raises { VerificationException.E _ -> not (RVSpec.grp_eq_up_to_rang_appel grp_e grp_s) } = if not (get_c_gp_cod grp_e = get_c_gp_cod grp_s) then raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_CGPCOD_DIFFERENTS (get_c_gp_cod grp_e) (get_c_gp_cod grp_s)); if not (get_taux_min_boursiers_pourcents grp_e = get_taux_min_boursiers_pourcents grp_s) then raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_TX_B_DIFFERENTS (get_taux_min_boursiers_pourcents grp_e) (get_taux_min_boursiers_pourcents grp_s)); if not (get_taux_min_du_secteur_pourcents grp_e = get_taux_min_du_secteur_pourcents grp_s) then raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_TX_R_DIFFERENTS (get_taux_min_du_secteur_pourcents grp_e) (get_taux_min_du_secteur_pourcents grp_s)); if not (get_nb_voeux_classes grp_e = get_nb_voeux_classes grp_s) then raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_NB_VOEUX_DIFFERENTS (get_nb_voeux_classes grp_e) (get_nb_voeux_classes grp_s) ); let nb_vc = get_nb_voeux_classes grp_e in let cp_e = get_ordre_pedagogique grp_e in let cp_s = get_ordre_pedagogique grp_s in try for i = 0 to nb_vc - 1 do invariant { forall k. 0 <= k < i -> VoeuClasse_Props.voeux_classes_eq_up_to_rang_appel cp_e[k] cp_s[k] } let ve = UL.get cp_e i in let vs = UL.get cp_s i in if not VoeuClasse.eq_up_to_rang_appel ve vs then raise VerificationException.E (crtX2 VerificationExceptionMessage.VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_DONNEES_ENTREE_SORTIE_INCOHERENTS (VoeuClasse.get_g_cn_cod ve) (VoeuClasse.get_g_cn_cod vs)); done with IndexOutOfBoundsException.E _ -> absurd end let verifier (entree : AOAE.t) (sortie : AOAS.t) : unit ensures { RVSpec.donnees_entree_eq_sortie entree sortie } ensures { RVSpec.groups_satisfy_specs sortie } raises { VerificationException.E _ -> not (RVSpec.donnees_entree_eq_sortie entree sortie) \/ not (RVSpec.groups_satisfy_specs sortie) } = let e_gp_cods = AOAE.get_c_gp_cods_map entree in let nb_g = AOAE.get_nb_groupes entree in if nb_g <> AOAS.get_nb_groupes sortie then raise VerificationException.E (crtX0 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_TAILLES_DONNEES_ENTREE_SORTIE_INCOHERENTS); try begin for i = 0 to nb_g - 1 do invariant { forall k. 0 <= k < i -> exists j. 0 <= j < nb_g && RVSpec.grp_eq_up_to_rang_appel entree[j] sortie[k] } invariant { RVSpec.groups_satisfy_specs_loc sortie i } let grp_s = AOAS.get_ith_groupe sortie i in let c_gp_cod : integer = get_c_gp_cod grp_s in if not (Map.containsKey e_gp_cods c_gp_cod) then raise VerificationException.E (crtX0 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_DONNEE_SORTIE_MANQUANTE); let e_i = Map.get e_gp_cods c_gp_cod in let grp_e = AOAE.get_ith_groupe entree e_i in assert { c_gp_cod = get_c_gp_cod grp_e }; verifier_coherence_donnees_entree_sortie grp_e grp_s; verifier_rangs_appel grp_s; VerifP1.verifier grp_s; VerifP2.verifier grp_s; VerifP3.verifier grp_s; VerifP4.verifier grp_s; VerifP5.verifier grp_s; done; end with | InvalidArgumentException.E _ -> absurd end end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git