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