Parcoursup / Calcul de l'ordre d'appel des candidats index
module RuntimeVerificationSpecP3 use seq.Seq use int.Int use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide predicate p3a_aux (s : seq VoeuClasse.t) (i k : int) = est_boursier s[k] || get_rang s[k] <= get_rang s[i] || get_rang_appel s[k] >= get_rang_appel s[i] predicate p3a_loc (s : seq VoeuClasse.t) (tx_r : Taux.t) (i : int) = (not (est_boursier s[i]) && (est_du_secteur s[i] || tx_r = 0)) -> (forall k. 0 <= k < length s -> p3a_aux s i k) predicate rang_appel_correct_p (q_b rang rang_appel : int) = ((100 - q_b) * rang_appel <= (100 - q_b) + 100 * rang) predicate p3b_loc (s : seq VoeuClasse.t) (tx_b tx_r : Taux.t) (i : int) = not (est_boursier s[i]) && (est_du_secteur s[i] || tx_r = 0) -> rang_appel_correct_p tx_b (get_rang s[i]) (get_rang_appel s[i]) predicate spec (grp : GroupeClassementValide.t) = let s = get_ordre_appel_list grp in let tx_b = get_taux_min_boursiers grp in tx_b < 100 -> let tx_r = get_taux_min_du_secteur grp in forall i. 0 <= i < length s -> (p3a_loc s tx_r i && p3b_loc s tx_b tx_r i) end module RuntimeVerificationSpecP3_LocalLemmas use mach.java.lang.Integer use int.Int use seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use proofs.ordre_appel.properties.q4_1.Q4_1 use proofs.ordre_appel.properties.q5.Q5 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 RuntimeVerificationSpecP3 let lemma l1a (grp : GroupeClassementValide.t) (s : seq_voeu) (i : int) requires { ordre_appel_properties grp } requires { s == get_ordre_appel_list grp } requires { 0 <= i < length s } requires { est_non_boursier_du_secteur s[i] } ensures { p3a_loc s (get_taux_min_du_secteur grp) i } = begin assert { q4_1a s }; assert { q4_1a_loc s i }; for k = 0 to length s - 1 do invariant { forall j. 0 <= j < k -> p3a_aux s i j } if est_boursier s[k] then continue; if est_du_secteur s[k] then begin assert { est_non_boursier_du_secteur s[k] }; assert { p3a_aux s i k }; end; assert { p3a_aux s i k }; done end let lemma l1b (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b : Taux.t) (i : int) requires { ordre_appel_properties grp } requires { ordre_appel_contiguous grp } requires { s == get_ordre_appel_list grp } requires { 0 <= i < length s } requires { est_non_boursier_du_secteur s[i] } requires { tx_b = get_taux_min_boursiers grp } ensures { p3b_loc s tx_b (get_taux_min_du_secteur grp) i } = begin assert { q4_1 (nb_boursiers s) tx_b s }; assert { q4_1b_loc tx_b s i }; assert { rang_appel_correct_p tx_b (get_rang s[i]) (get_rang_appel s[i]) } end let lemma l2a (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b tx_ds : Taux.t) (i : int) requires { ordre_appel_properties grp } requires { s == get_ordre_appel_list grp } requires { 0 <= i < length s } requires { est_non_boursier_hors_secteur s[i] } requires { tx_b = get_taux_min_boursiers grp } requires { tx_ds = get_taux_min_du_secteur grp = 0 } ensures { p3a_loc s tx_ds i } = let nb_b = nb_boursiers s in let nb_ds = nb_du_secteur s in assert { q5 nb_b nb_ds tx_b tx_ds s }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s i }; assert { forall k. 0 <= k < length s -> not in_Zr nb_ds tx_ds s k }; for k = 0 to length s - 1 do invariant { forall j. 0 <= j < k -> p3a_aux s i j } if est_boursier s[k] || i <= k then continue; if get_rang s[k] > get_rang s[i] then begin assert { in_Zb nb_b tx_b s k }; absurd; end done let lemma l2b (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b tx_ds : Taux.t) (i : int) requires { ordre_appel_properties grp } requires { ordre_appel_contiguous grp } requires { s == get_ordre_appel_list grp } requires { 0 <= i < length s } requires { est_non_boursier_hors_secteur s[i] } requires { tx_b = get_taux_min_boursiers grp < 100 } requires { tx_ds = get_taux_min_du_secteur grp = 0 } ensures { p3b_loc s tx_b tx_ds i } = let nb_b = nb_boursiers s in let nb_ds = nb_du_secteur s in assert { nb_contraintes_taux_ds nb_ds tx_ds s[..i] = 0 }; assert { q5 nb_b nb_ds tx_b tx_ds s }; assert { q5b_loc tx_b tx_ds s i }; assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s i }; assert { iq4_2a nb_b tx_b s }; assert { iq4_2a_loc nb_b tx_b s i }; () end module RuntimeVerificationSpecP3_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 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 RuntimeVerificationSpecP3_LocalLemmas use export RuntimeVerificationSpecP3 let lemma spec_imply_rv_p3 (grp : GroupeClassementValide.t) requires { ordre_appel_properties grp } requires { ordre_appel_contiguous grp } ensures { spec grp } = let tx_b = get_taux_min_boursiers grp in if Integer.to_int (Taux.tx tx_b) >= 100 then return; let tx_ds = get_taux_min_du_secteur grp in let s = UL.content (get_ordre_appel_list grp) in for i = 0 to Seq.length s - 1 do invariant { forall j. 0 <= j < i -> p3a_loc s tx_ds j } invariant { forall j. 0 <= j < i -> p3b_loc s tx_b tx_ds j } if est_boursier s[i] then continue; if est_du_secteur s[i] then begin assert { est_non_boursier_du_secteur s[i] }; assert { p3a_loc s tx_ds i }; assert { p3b_loc s tx_b tx_ds i }; end else if Integer.to_int (Taux.tx tx_ds) = 0 then begin assert { est_non_boursier_hors_secteur s[i] }; assert { p3a_loc s tx_ds i }; assert { p3b_loc s tx_b tx_ds i }; end done end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git