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/Java/openclaw/ (KI Agentensystem Version 22^©) Datei vom 18.1.2026 mit Größe 54 B

Quelle Hotel_Example.thy Sprache: Isabelle

theory Hotel_Example
imports Main "HOL-Library.Predicate_Compile_Quickcheck"
begin

datatype guest = Guest0 | Guest1
datatype key = Key0 | Key1 | Key2 | Key3
datatype room = Room0

type_synonym card = "key * key"

datatype event =
  Check_in guest room card
| Enter guest room card
| Exit guest room

definition initk :: "room \ key"
  where "initk = (%r. Key0)"

declare initk_def[code_pred_def, code]

primrec owns :: "event list \ room \ guest option"
where
  "owns [] r = None"
| "owns (e#s) r = (case e of
    Check_in g r' c \ if r' = r then Some g else owns s r |
    Enter g r' c \ owns s r |
    Exit g r' \ owns s r)"

primrec currk :: "event list \ room \ key"
where
  "currk [] r = initk r"
| "currk (e#s) r = (let k = currk s r in
    case e of Check_in g r' (k1, k2) \ if r' = r then k2 else k
            | Enter g r' c \ k
            | Exit g r \<Rightarrow> k)"

primrec issued :: "event list \ key set"
where
  "issued [] = range initk"
| "issued (e#s) = issued s \
  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"

primrec cards :: "event list \ guest \ card set"
where
  "cards [] g = {}"
| "cards (e#s) g = (let C = cards s g in
                    case e of Check_in g' r c \ if g' = g then insert c C
                                                else C
                            | Enter g r c \<Rightarrow> C
                            | Exit g r \<Rightarrow> C)"

primrec roomk :: "event list \ room \ key"
where
  "roomk [] r = initk r"
| "roomk (e#s) r = (let k = roomk s r in
    case e of Check_in g r' c \ k
            | Enter g r' (x,y) \ if r' = r \<^cancel>\\ x = k\ then y else k
            | Exit g r \<Rightarrow> k)"

primrec isin :: "event list \ room \ guest set"
where
  "isin [] r = {}"
| "isin (e#s) r = (let G = isin s r in
                 case e of Check_in g r c \<Rightarrow> G
                 | Enter g r' c \ if r' = r then {g} \ G else G
                 | Exit g r' \ if r'=r then G - {g} else G)"

primrec hotel :: "event list \ bool"
where
  "hotel [] = True"
| "hotel (e # s) = (hotel s & (case e of
  Check_in g r (k,k') \ k = currk s r \ k' \ issued s |
  Enter g r (k,k') \ (k,k') \ cards s g & (roomk s r \ {k, k'}) |
  Exit g r \<Rightarrow> g \<in> isin s r))"

definition no_Check_in :: "event list \ room \ bool" where(*>*)
[code del]: "no_Check_in s r \ \(\g c. Check_in g r c \ set s)"

definition feels_safe :: "event list \ room \ bool"
where
  "feels_safe s r = (\s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
   s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
   no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"

section \<open>Some setup\<close>

lemma issued_nil: "issued [] = {Key0}"
by (auto simp add: initk_def)

lemmas issued_simps[code] = issued_nil issued.simps(2)

setup \<open>Predicate_Compile_Data.ignore_consts [\<^const_name>\<open>Set.member\<close>,
  \<^const_name>\<open>issued\<close>, \<^const_name>\<open>cards\<close>, \<^const_name>\<open>isin\<close>,
  \<^const_name>\<open>Collect\<close>, \<^const_name>\<open>insert\<close>]\<close>
ML_val \<open>Core_Data.force_modes_and_compilations\<close>

fun find_first :: "('a => 'b option) => 'a list => 'b option"
where
  "find_first f [] = None"
| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"

axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"

axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"

axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
    => 'b list => 'a Quickcheck_Exhaustive.three_valued"
where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
  and find_first'_Cons: "find_first' f (x # xs) =
    (case f (Quickcheck_Exhaustive.Known x) of
      Quickcheck_Exhaustive.No_value => find_first' f xs
    | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
    | Quickcheck_Exhaustive.Unknown_value =>
        (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
          Quickcheck_Exhaustive.Value x
        | _ => Quickcheck_Exhaustive.Unknown_value))"

lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons

axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"

setup \<open>
let
  val Fun = Predicate_Compile_Aux.Fun
  val Input = Predicate_Compile_Aux.Input
  val Output = Predicate_Compile_Aux.Output
  val Bool = Predicate_Compile_Aux.Bool
  val oi = Fun (Output, Fun (Input, Bool))
  val ii = Fun (Input, Fun (Input, Bool))
  fun of_set compfuns \<^Type>\<open>fun T _\<close> =
    case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
      \<^Type>\<open>Quickcheck_Exhaustive.three_valued _\<close> =>
        Const(\<^const_name>\<open>neg_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
    | _ => Const(\<^const_name>\<open>pos_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
  fun member compfuns (U as \<^Type>\<open>fun T _\<close>) =
    (absdummy T (absdummy \<^Type>\<open>set T\<close> (Predicate_Compile_Aux.mk_if compfuns
      (\<^Const>\<open>Set.member T for \<open>Bound 1\<close> \<open>Bound 0\<close>\<close>))))

in
  Core_Data.force_modes_and_compilations \<^const_name>\<open>Set.member\<close>
    [(oi, (of_set, false)), (ii, (member, false))]
end
\<close>
section \<open>Property\<close>

lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g"
quickcheck[tester = exhaustive, size = 6, expect = counterexample]
quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
oops

lemma
  "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g"
quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
oops

section \<open>Refinement\<close>

fun split_list
where
  "split_list [] = [([], [])]"
| "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"

lemma split_list: "((xs, ys) \ set (split_list zs)) = (zs = xs @ ys)"
apply (induct zs arbitrary: xs ys)
apply fastforce
apply (case_tac xs)
apply auto
done

lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r \ r' | _ => True) s"
unfolding no_Check_in_def list_all_iff
apply auto
apply (case_tac x)
apply auto
done

lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
    isin (s2 @ [Check_in g r c] @ s1) r = {}) ([(s3, s2, s1, g, c, c'). (s3, Enter g' r' c # r3) <- split_list s, r' = r, (s2, Check_in g r'' c' # s1) <- split_list r3, r'' = r, g = g'])"
unfolding feels_safe_def list_ex_iff
by auto (metis split_list)+

lemma
  "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g"
(* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
quickcheck[narrowing, size = 7, expect = counterexample]
oops

end

quality87%

¤ 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.