products/sources/formale sprachen/Isabelle/HOL/TLA/Buffer/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Buffer.thy   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/TLA/Buffer/Buffer.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>

theory Buffer
imports "HOL-TLA.TLA"
begin

(* actions *)

definition BInit :: "'a stfun \ 'a list stfun \ 'a stfun \ stpred"
  where "BInit ic q oc == PRED q = #[]"

definition Enq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Enq ic q oc == ACT (ic$ \ $ic)
                         \<and> (q$ = $q @ [ ic$ ])
                         \<and> (oc$ = $oc)"

definition Deq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Deq ic q oc == ACT ($q \ #[])
                         \<and> (oc$ = hd< $q >)
                         \<and> (q$ = tl< $q >)
                         \<and> (ic$ = $ic)"

definition Next :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
  where "Next ic q oc == ACT (Enq ic q oc \ Deq ic q oc)"


(* temporal formulas *)

definition IBuffer :: "'a stfun \ 'a list stfun \ 'a stfun \ temporal"
  where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
                                  \<and> \<box>[Next ic q oc]_(ic,q,oc)
                                  \<and> WF(Deq ic q oc)_(ic,q,oc)"

definition Buffer :: "'a stfun \ 'a stfun \ temporal"
  where "Buffer ic oc == TEMP (\\q. IBuffer ic q oc)"


(* ---------------------------- Data lemmas ---------------------------- *)

(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
lemma tl_not_self [simp]: "xs \ [] \ tl xs \ xs"
  by (auto simp: neq_Nil_conv)


(* ---------------------------- Action lemmas ---------------------------- *)

(* Dequeue is visible *)
lemma Deq_visible: "\ _(ic,q,oc) = Deq ic q oc"
  apply (unfold angle_def Deq_def)
  apply (safe, simp (asm_lr))+
  done

(* Enabling condition for dequeue -- NOT NEEDED *)
lemma Deq_enabled: 
    "\q. basevars (ic,q,oc) \ \ Enabled (_(ic,q,oc)) = (q \ #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
  done

(* For the left-to-right implication, we don't need the base variable stuff *)
lemma Deq_enabledE: 
    "\ Enabled (_(ic,q,oc)) \ (q \ #[])"
  apply (unfold Deq_visible [temp_rewrite])
  apply (auto elim!: enabledE simp add: Deq_def)
  done

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff