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