Parcoursup / Calcul de l'ordre d'appel des candidats index
module AlgoOrdreAppelDonneesClone [@java:package:fr.parcoursup.whyml.ordreappel.algo] use int.Int use seq.Seq use mach.java.util.Set use mach.java.util.Map use mach.java.util.List use mach.java.util.UnmodifiableList as UL use mach.java.lang.Integer use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe 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.ordreappel.algo.groupe_classement.GroupeClassement use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide use fr.parcoursup.whyml.ordreappel.algo.list_groupe_classement_valide.ListGroupeClassementValide type t [@extraction:preserve_single_field] = { aoad_groupes_classements : list GroupeClassementValide.t; } invariant { [@expl:groupes ok] forall i. 0 <= i < List.size aoad_groupes_classements -> groupe_ok aoad_groupes_classements[i] } invariant { [@expl:c_gp_cod uniques] forall i j. 0 <= i < List.size aoad_groupes_classements -> 0 <= j < List.size aoad_groupes_classements -> i <> j -> get_c_gp_cod aoad_groupes_classements[i] <> get_c_gp_cod aoad_groupes_classements[j] } invariant { Seq.length aoad_groupes_classements < Integer.max_integer } by { aoad_groupes_classements = List.empty (); } meta coercion function aoad_groupes_classements let algo_ordre_appel_donnees [@java:constructor] () : t = { aoad_groupes_classements = List.empty (); } let function get_nb_groupes (self : t) : integer ensures { result = Integer.enforced_integer (Seq.length self) } = List.size self.aoad_groupes_classements let function get_ith_groupe_safe [@java:visibility:package] (self : t) (i : integer) : GroupeClassementValide.t requires { 0 <= i < get_nb_groupes self } ensures { result = self[i] } = try List.get self.aoad_groupes_classements i with IndexOutOfBoundsException.E _ -> absurd end let get_ith_groupe (self : t) (i : integer) : GroupeClassementValide.t ensures { result = self[i] } raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_groupes self) } = if (not (0 <= i && i < get_nb_groupes self)) then raise InvalidArgumentException.E (index_out_of_bounds i); get_ith_groupe_safe self i let function get_ith_c_gp_cod_safe [@java:visibility:package] (self : t) (i : integer) : integer requires { 0 <= i < get_nb_groupes self } ensures { result = get_c_gp_cod self[i] } = get_c_gp_cod (get_ith_groupe_safe self i) let get_ith_c_gp_cod (self : t) (i : integer) : integer ensures { result = get_c_gp_cod self[i] } raises { InvalidArgumentException.E _ -> not (0 <= i < get_nb_groupes self) } = get_c_gp_cod (get_ith_groupe self i) let add_groupe_valide (self : t) (grp : GroupeClassementValide.t) : unit ensures { get_nb_groupes self = get_nb_groupes (old self) + 1 } ensures { self[(get_nb_groupes self) - 1] = grp } ensures { forall i. 0 <= i < (get_nb_groupes self) - 1 -> self[i] = (old self)[i] } raises { VerificationException.E _ -> (exists i. 0 <= i < (get_nb_groupes (old self)) && get_c_gp_cod grp = get_c_gp_cod (old self)[i]) \/ get_nb_groupes (old self) >= Integer.max_integer - 1 } = if (get_nb_groupes self >= Integer.max_integer - 1) then raise VerificationException.E (crtX0 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_POSSIBLE_DEPASSEMENT_ARITHMETIQUE); let nb_groupes = get_nb_groupes self in for i = 0 to nb_groupes - 1 do invariant { forall k. 0 <= k < i -> get_c_gp_cod self[k] <> get_c_gp_cod grp } if get_ith_c_gp_cod_safe self i = get_c_gp_cod grp then raise VerificationException.E (crtX1 VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_GCNCOD_DUPLIQUE (get_c_gp_cod grp)); done; let _ = List.add self.aoad_groupes_classements grp in () let add_groupe (self : t) (grp : GroupeClassement.t) : unit ensures { get_nb_groupes self = get_nb_groupes (old self) + 1 } ensures { gcv_eq_gc self[(get_nb_groupes self) - 1] grp } ensures { forall i. 0 <= i < (get_nb_groupes self) - 1 -> self[i] = (old self)[i] } raises { VerificationException.E _ -> (exists i. GroupeClassement.get_c_gp_cod grp = get_c_gp_cod (old self)[i]) \/ not (GroupeClassement.groupe_ok grp) \/ get_nb_groupes (old self) >= Integer.max_integer - 1 } = add_groupe_valide self (groupe_classement_valide grp) let function get_c_gp_cods_map (self : t) : (res : Map.map integer integer) ensures { Map.size res = get_nb_groupes self } ensures { forall i. 0 <= i < get_nb_groupes self -> Map.containsKey res (get_c_gp_cod self[i]) } ensures { forall i. 0 <= i < get_nb_groupes self -> Map.get res (get_c_gp_cod self[i]) = i } ensures { forall c : integer. Map.containsKey res c -> 0 <= Map.get res c < get_nb_groupes self } ensures { forall c : integer. Map.containsKey res c -> let i = Map.get res c in c = get_c_gp_cod self[i] } = let nb_groupes = get_nb_groupes self in let res = Map.empty () in for i = 0 to nb_groupes - 1 do invariant { forall j. 0 <= j < i -> Map.containsKey res (get_c_gp_cod self[j]) } invariant { forall j. i <= j < nb_groupes -> not Map.containsKey res (get_c_gp_cod self[j]) } invariant { forall j. 0 <= j < i -> Map.get res (get_c_gp_cod self[j]) = j } invariant { forall c : integer. Map.containsKey res c -> 0 <= Map.get res c < i } invariant { forall c : integer. Map.containsKey res c -> exists k. 0 <= k < i /\ k = Map.get res c } invariant { forall c : integer. Map.containsKey res c -> c = get_c_gp_cod self[Map.get res c] } invariant { Map.size res = i } let grp = get_ith_groupe_safe self i in let c_gp_cod = get_c_gp_cod grp in label H in let ores = pure { res at H } in assert { not Map.containsKey res c_gp_cod }; assert { forall c. c <> c_gp_cod -> Map.containsKey ores c -> 0 <= Map.get ores c < i }; Map.put res c_gp_cod i; assert { forall c. c <> c_gp_cod -> Map.containsKey res c -> Map.containsKey ores c }; assert { forall c. c <> c_gp_cod -> Map.containsKey res c -> 0 <= Map.get res c < i }; assert { Map.containsKey res c_gp_cod && Map.get res c_gp_cod = i }; done; res end (* generated on Mon Dec 2 02:04:28 UTC 2024 from rev: *)
Generated by why3doc 1.7.2+git