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