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/SPARK/Examples/RIPEMD-160/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 970 B

Quelle K_L.thy Sprache: Isabelle

(*  Title:      HOL/SPARK/Examples/RIPEMD-160/K_L.thy
    Author:     Fabian Immler, TU Muenchen

Verification of the RIPEMD-160 hash function
*)

theory K_L
imports RMD_Specification
begin

spark_open \<open>rmd/k_l\<close>

spark_vc function_k_l_6
  using assms by (simp add: K_def)

spark_vc function_k_l_7
proof -
  from H1 have "16 <= nat j" by simp
  moreover from H2 have "nat j <= 31" by simp
  ultimately show ?thesis by (simp add: K_def)
qed

spark_vc function_k_l_8
proof -
  from H1 have "32 <= nat j" by simp
  moreover from H2 have "nat j <= 47" by simp
  ultimately show ?thesis by (simp add: K_def)
qed

spark_vc function_k_l_9
proof -
  from H1 have "48 <= nat j" by simp
  moreover from H2 have "nat j <= 63" by simp
  ultimately show ?thesis by (simp add: K_def)
qed

spark_vc function_k_l_10
proof -
  from H6 have "64 <= nat j" by simp
  moreover from H2 have "nat j <= 79" by simp
  ultimately show ?thesis by (simp add: K_def)
qed

spark_end

end

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

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.