Parcoursup / Calcul de l'ordre d'appel des candidats index
(* https://framagit.org/parcoursup/algorithmes-de-parcoursup/-/tree/master/src/main/java/fr/parcoursup/algos/ordreappel/algo/OrdreAppel.java *) module OrdreAppel [@java:package:fr.parcoursup.whyml.ordreappel.algo] use int.Int use seq.Seq use mach.java.lang.Integer use mach.java.util.List use mach.java.util.UnmodifiableList as UL use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe use fr.parcoursup.whyml.ordreappel.algo.candidat_classe.CandidatClasse as CC use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse as VC use fr.parcoursup.whyml.exceptions.invalid_argument_exception.InvalidArgumentException type t [@extraction:preserve_single_field] = { candidats : UL.ulist CC.t; } invariant { [@expl:rang_appel tries] forall i j. 0 <= i < j < Seq.length candidats -> CC.get_rang_appel candidats[i] < CC.get_rang_appel candidats[j] } invariant { [@expl:g_cn_cod unique] forall i j. 0 <= i < Seq.length candidats -> 0 <= j < Seq.length candidats -> i <> j -> CC.get_g_cn_cod candidats[i] <> CC.get_g_cn_cod candidats[j] } invariant { [@expl:g_cn_cod >= 0] forall i. 0 <= i < Seq.length candidats -> CC.get_g_cn_cod candidats[i] >= 0 } invariant { [@expl:rang appel >= 0] forall i. 0 <= i < Seq.length candidats -> CC.get_rang_appel candidats[i] >= 0 } invariant { [@expl:|oa| <= max_integer] Seq.length candidats <= Integer.max_integer } by { candidats = UL.empty (); } meta coercion function candidats let function get_nb_candidats (self : t) : integer ensures { result = Seq.length self } = UL.size self.candidats let get_ith_candidat_classe (self : t) (i : integer) : CC.t ensures { result = self[i] } raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) } = if (not (0 <= i && i < get_nb_candidats self)) then raise InvalidArgumentException.E (index_out_of_bounds i); try UL.get self.candidats i with IndexOutOfBoundsException.E _ -> absurd end let get_ith_g_cn_cod (self : t) (i : integer) : integer ensures { result = CC.get_g_cn_cod self[i] } raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) } = CC.get_g_cn_cod (get_ith_candidat_classe self i) let get_ith_rang_appel (self : t) (i : integer) : integer ensures { result = CC.get_rang_appel self[i] } raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_candidats self) } = CC.get_rang_appel (get_ith_candidat_classe self i) let function ordre_appel [@java:constructor] [@java:visibility:package] (voeux : UL.ulist VC.t) : t requires { [@expl:pre |voeux| <= max_integer] UL.size voeux <= Integer.max_integer } requires { [@expl:pre c_gn_cod >= 0] seq_g_cn_cod_ge_0 voeux } requires { [@expl:pre rang_appel >= 1] seq_rangs_appel_ge_1 voeux } requires { [@expl:pre g_cn_cod unique] seq_g_cn_cod_uniques voeux } requires { [@expl:pre rang_appel ordonnes] seq_rangs_appel_sorted voeux } ensures { [@expl:|res|=|voeux|] get_nb_candidats result = UL.size voeux } ensures { [@expl:rang_appel tries] forall i j. 0 <= i < j < UL.size result.candidats -> CC.get_rang_appel result[i] < CC.get_rang_appel result[j] } ensures { [@expl:res eq input] forall i. 0 <= i < UL.size voeux -> CC.est_voeu_classe result[i] voeux[i] } ensures { [@expl: g_cn_cod unique] forall i j. 0 <= i < UL.size voeux -> 0 <= j < UL.size voeux -> i <> j -> CC.get_g_cn_cod result[i] <> CC.get_g_cn_cod result[j] } = try let lvc : list CC.t = List.empty () in let len = UL.size voeux in for i = 0 to len - 1 do invariant { Seq.length lvc = i } invariant { forall j. 0 <= j < i -> CC.get_rang_appel lvc[j] = VC.get_rang_appel voeux[j] } invariant { forall j. 0 <= j < i -> CC.get_g_cn_cod lvc[j] = VC.get_g_cn_cod voeux[j] } invariant { forall k l. 0 <= k < i -> 0 <= l < i -> k <> l -> CC.get_rang_appel lvc[k] <> CC.get_rang_appel lvc[l] } invariant { forall k l. 0 <= k < i -> 0 <= l < i -> k <> l -> CC.get_g_cn_cod lvc[k] <> CC.get_g_cn_cod lvc[l] } let vc = UL.get voeux i in let cc = CC.candidat_classe (VC.get_g_cn_cod vc) (VC.get_rang_appel vc) in let _ = List.add lvc cc in (); done; { candidats = List.copy_of lvc; } with IndexOutOfBoundsException.E _ -> absurd end end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git