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/UNITY/Comp/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle TimerArray.thy Sprache: Isabelle

(*  Title:      HOL/UNITY/Comp/TimerArray.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

A trivial example of reasoning about an array of processes
*)

theory TimerArray imports "../UNITY_Main" begin

type_synonym 'a state = "nat * 'a" (*second component allows new variables*)

definition count :: "'a state => nat"
  where "count s = fst s"

definition decr  :: "('a state * 'a state) set"
  where "decr = (UN n uu. {((Suc n, uu), (n,uu))})"

definition Timer :: "'a state program"
  where "Timer = mk_total_program (UNIV, {decr}, UNIV)"

declare Timer_def [THEN def_prg_Init, simp]

declare count_def [simp] decr_def [simp]

(*Demonstrates induction, but not used in the following proof*)
lemma Timer_leadsTo_zero: "Timer \ UNIV leadsTo {s. count s = 0}"
apply (rule_tac f = count in lessThan_induct, simp)
apply (case_tac "m")
apply (force intro!: subset_imp_leadsTo)
apply (unfold Timer_def, ensures_tac "decr")
done

lemma Timer_preserves_snd [iff]: "Timer \ preserves snd"
apply (rule preservesI)
apply (unfold Timer_def, safety)
done

declare PLam_stable [simp]

lemma TimerArray_leadsTo_zero:
     "finite I
      \<Longrightarrow> (plam i: I. Timer) \<in> UNIV leadsTo {(s,uu). \<forall>i\<in>I. s i = 0}"
apply (erule_tac A'1 = "\i. lift_set i ({0} \ UNIV)"
       in finite_stable_completion [THEN leadsTo_weaken])
apply auto
(*Safety property, already reduced to the single Timer case*)
prefer 2
apply (simp add: Timer_def, safety)
(*Progress property for the array of Timers*)
apply (rule_tac f = "sub i o fst" in lessThan_induct)
apply (case_tac "m")
(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
apply (auto intro: subset_imp_leadsTo
        simp add: insert_absorb
                  lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric]
               Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
apply (rename_tac "n")
apply (rule PLam_leadsTo_Basis)
apply (auto simp add: lessThan_Suc [symmetric])
apply (unfold Timer_def mk_total_program_def, safety)
apply (rule_tac act = decr in totalize_transientI, auto)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.14 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.