module CandidatClasse
    [@java:package:fr.parcoursup.whyml.ordreappel.algo]

    use int.Int
    use mach.java.lang.Integer
    use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse as VC

    type t [@java:visibility:private] = {
        cc_g_cn_cod : integer;
        cc_rang_appel : integer;
    } invariant {
        0 <= cc_g_cn_cod
    } invariant {
        0 <= cc_rang_appel
    } by { cc_g_cn_cod = 0; cc_rang_appel = 0 }

    let candidat_classe [@java:constructor] [@java:visibility:package] (cod : integer) (rang : integer) : t
        requires { 0 <= cod }
        requires { 0 <= rang }
    = { cc_g_cn_cod = cod; cc_rang_appel = rang; }

    let function get_g_cn_cod (self : t) : integer
        ensures { 0 <= result  }
      = self.cc_g_cn_cod

    let function get_rang_appel (self : t) : integer
        ensures { 0 <= result  }
      = self.cc_rang_appel

    let function est_voeu_classe (self : t) (vc : VC.t) : bool
        ensures { result <->
                   ((get_g_cn_cod self = VC.get_g_cn_cod vc) &&
                    (get_rang_appel self = VC.get_rang_appel vc)) }
    = self.cc_g_cn_cod = VC.get_g_cn_cod vc &&
      self.cc_rang_appel = VC.get_rang_appel vc
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)