Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek Proc1.thy   Sprache: Isabelle

 
theory Proc1
imports "HOL-SPARK.SPARK"
begin

spark_open \<open>loop_invariant/proc1\<close>

spark_vc procedure_proc1_5
  by (simp add: ring_distribs mod_simps)

spark_vc procedure_proc1_8
  by (simp add: ring_distribs mod_simps)

spark_end

lemma pow_2_32_simp: "4294967296 = (2::int)^32"
  by simp

end

100%


¤ 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.0.0Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff






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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.