added abstract;corrected RG_Basic Hoare rule.
authorprensani
Mon Apr 29 16:45:12 2002 +0200 (2002-04-29)
changeset 130994bb592cdde0e
parent 13098 e0644528e21e
child 13100 ff00791319e2
added abstract;corrected RG_Basic Hoare rule.
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/HoareParallel/RG_Syntax.thy
src/HOL/HoareParallel/document/root.tex
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 11:30:15 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 16:45:12 2002 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4    \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
     1.5      (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i)\<rbrace>]"
     1.6  apply(rule Parallel)
     1.7 -(*5*)
     1.8 +--{*5 subgoals left *}
     1.9  apply force+
    1.10  apply clarify
    1.11  apply simp
    1.12 @@ -372,7 +372,7 @@
    1.13        \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
    1.14          (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
    1.15  apply(rule Parallel)
    1.16 -(*5*)
    1.17 +--{* 5 subgoals left *}
    1.18  apply force+
    1.19  apply clarify
    1.20  apply simp
     2.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Apr 29 11:30:15 2002 +0200
     2.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Apr 29 16:45:12 2002 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  inductive rghoare
     2.6  intros
     2.7 -  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> t=f s} \<subseteq> guar; 
     2.8 +  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
     2.9              stable pre rely; stable post rely \<rbrakk> 
    2.10             \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
    2.11  
     3.1 --- a/src/HOL/HoareParallel/RG_Syntax.thy	Mon Apr 29 11:30:15 2002 +0200
     3.2 +++ b/src/HOL/HoareParallel/RG_Syntax.thy	Mon Apr 29 16:45:12 2002 +0200
     3.3 @@ -1,3 +1,5 @@
     3.4 +
     3.5 +header {* \section{Concrete Syntax} *}
     3.6  
     3.7  theory RG_Syntax = RG_Hoare + Quote_Antiquote:
     3.8  
     4.1 --- a/src/HOL/HoareParallel/document/root.tex	Mon Apr 29 11:30:15 2002 +0200
     4.2 +++ b/src/HOL/HoareParallel/document/root.tex	Mon Apr 29 16:45:12 2002 +0200
     4.3 @@ -18,6 +18,26 @@
     4.4  \author{Leonor Prensa Nieto}
     4.5  \maketitle
     4.6  
     4.7 +\begin{abstract}\noindent
     4.8 +  In the following theories a formalization of the Owicki-Gries and
     4.9 +  the rely-guarantee methods is presented. These methods are widely
    4.10 +  used for correctness proofs of parallel imperative programs with
    4.11 +  shared variables.  We define syntax, semantics and proof rules in
    4.12 +  Isabelle/HOL.  The proof rules also provide for programs
    4.13 +  parameterized in the number of parallel components. Their
    4.14 +  correctness w.r.t.\ the semantics is proven.  Completeness proofs
    4.15 +  for both methods are extended to the new case of parameterized
    4.16 +  programs. (These proofs have not been formalized in Isabelle. They
    4.17 +  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
    4.18 +  verify several non-trivial examples for parameterized and
    4.19 +  non-parameterized programs.  For the automatic generation of
    4.20 +  verification conditions with the Owicki-Gries method we define a
    4.21 +  tactic based on the proof rules.  The most involved examples are the
    4.22 +  verification of two garbage-collection algorithms, the second one
    4.23 +  parameterized in the number of mutators.
    4.24 +
    4.25 +\end{abstract}
    4.26 +
    4.27  \pagestyle{plain}
    4.28  \thispagestyle{empty}
    4.29  \tableofcontents