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

  use int.Int
  use mach.java.lang.Integer
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  type t [@extraction:preserve_single_field] = {
    tx : integer;
  } invariant {
    0 <= tx <= 100
  } by {
    tx = 0;
  }

  let taux [@java:constructor] (tx : integer) : t
    ensures { result.tx = tx }
    raises { VerificationException.E _ -> not (0 <= tx <= 100) }
  = if not (0 <= tx <= 100) then
      raise VerificationException.E (crtX1 VerificationExceptionMessage.VERIFICATION_ENTREE_ALGO_ORDRE_APPEL_TAUX tx);
    { tx = tx; }

  let function taux_zero () : t
    ensures { result.tx = 0 }
  =
    try
      taux 0;
    with
      | VerificationException.E _ -> absurd
    end

  function to_int (taux : t) : int = taux.tx
  meta coercion function to_int

  let lemma to_int_in_range (taux : t)
    ensures { 0 <= to_int taux <= 100 }
  = ()

end

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