Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Tools/Mirabelle/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle mirabelle_util.ML Sprache: SML

(*  Title:      HOL/Tools/Mirabelle/mirabelle_util.ML
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

(* Pseudorandom number generator *)
signature PRNG = sig
  type state
  val initialize : int -> state
  val next : state -> int * state
end

(* Pseudorandom algorithms *)
signature PRNG_ALGORITHMS = sig
  include PRNG
  val shuffle : state -> 'a list -> 'a list * state
end

functor PRNG_Algorithms(PRNG : PRNG) : PRNG_ALGORITHMS = struct

open PRNG

fun shuffle prng_state xs =
  fold_map (fn x => fn prng_state =>
    let
      val (n, prng_state') = next prng_state
    in ((n, x), prng_state') end) xs prng_state
  |> apfst (sort (int_ord o apply2 fst))
  |> apfst (map snd)

end

(* multiplicative linear congruential generator *)
structure MLCG_PRNG : PRNG = struct
  (* The modulus is implicitly 2^64 through using Word64.
     The multiplier and increment are the same as Newlib and Musl according to Wikipedia.
     See: https://en.wikipedia.org/wiki/Linear_congruential_generator#Parameters_in_common_use
   *)
  val multiplier = Word64.fromInt 6364136223846793005
  val increment = Word64.fromInt 1

  type state = Word64.word

  val initialize = Word64.fromInt

  fun next s =
    let
      open Word64
      val s' = multiplier * s + increment
    in
      (toInt s', s')
    end
end

structure MLCG = PRNG_Algorithms(MLCG_PRNG)

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.