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


module RuntimeVerificationSpecP4
   use seq.Seq
   use int.Int

   use mach.java.lang.Integer
   use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
   use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide

   predicate p4a_aux (s : seq VoeuClasse.t) (i k : int) =
     est_du_secteur s[k] || get_rang s[k] <= get_rang s[i] ||
     get_rang_appel s[k] >= get_rang_appel s[i]

   predicate p4a_loc (s : seq VoeuClasse.t) (i : int) =
      (est_boursier s[i] && not (est_du_secteur s[i]))
      -> (forall k. 0 <= k < length s -> p4a_aux s i k)

   predicate rang_appel_correct_p (q_r rang rang_appel : int) =
      ((100 - q_r) * rang_appel <= (100 - q_r) + 100 * rang)

   predicate p4b_loc (s : seq VoeuClasse.t) (tx_ds : int) (i : int) =
     (est_boursier s[i] && not (est_du_secteur s[i]))
     -> rang_appel_correct_p tx_ds (get_rang s[i]) (get_rang_appel s[i])

   predicate spec (grp : GroupeClassementValide.t) =
     let s = get_ordre_appel_list grp in
     let tx_ds = get_taux_min_du_secteur_pourcents grp in
      tx_ds > 0 -> forall k. 0 <= k < length s -> (p4a_loc s k && p4b_loc s tx_ds k)
end

module RuntimeVerificationSpecP4_Lemmas
  use mach.java.lang.Integer
  use int.Int
  use mach.java.util.UnmodifiableList as UL
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.properties.q4_2.Q4_2

  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use export RuntimeVerificationSpecP4

  let lemma spec_imply_rv_p4 (grp : GroupeClassementValide.t)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }
    ensures { spec grp }
  =
    let tx_ds = get_taux_min_du_secteur grp in
    if Taux.tx tx_ds = 0 then
      return;
    let s = UL.content (get_ordre_appel_list grp) in
    let nb_ds = nb_du_secteur s in
    assert { q4_2 nb_ds tx_ds s };

    for i = 0 to Seq.length s - 1 do
      invariant { forall j. 0 <= j < i -> p4a_loc s j }
      invariant { forall j. 0 <= j < i -> p4b_loc s tx_ds j }

      if not est_boursier s[i] then continue;
      if est_du_secteur s[i] then continue;
      assert { est_boursier_hors_secteur s[i] };
      assert { q4_2a_loc s i };
      assert { q4_2b_loc tx_ds s i };
    done
end

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

Generated by why3doc 1.7.2+git