# HG changeset patch
# User prensani
# Date 1020091512 -7200
# Node ID 4bb592cdde0e13f059442d6754784aca7e56014a
# Parent  e0644528e21e7aee013e675fe836f0e6fdc2b6a6
added abstract;corrected RG_Basic Hoare rule.

diff -r e0644528e21e -r 4bb592cdde0e src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 11:30:15 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 16:45:12 2002 +0200
@@ -310,7 +310,7 @@
   \<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> 
     (\<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>]"
 apply(rule Parallel)
-(*5*)
+--{*5 subgoals left *}
 apply force+
 apply clarify
 apply simp
@@ -372,7 +372,7 @@
       \<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> 
         (\<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>]"
 apply(rule Parallel)
-(*5*)
+--{* 5 subgoals left *}
 apply force+
 apply clarify
 apply simp
diff -r e0644528e21e -r 4bb592cdde0e src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Apr 29 11:30:15 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Apr 29 16:45:12 2002 +0200
@@ -18,7 +18,7 @@
 
 inductive rghoare
 intros
-  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> t=f s} \<subseteq> guar; 
+  Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; 
             stable pre rely; stable post rely \<rbrakk> 
            \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
 
diff -r e0644528e21e -r 4bb592cdde0e src/HOL/HoareParallel/RG_Syntax.thy
--- a/src/HOL/HoareParallel/RG_Syntax.thy	Mon Apr 29 11:30:15 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Mon Apr 29 16:45:12 2002 +0200
@@ -1,3 +1,5 @@
+
+header {* \section{Concrete Syntax} *}
 
 theory RG_Syntax = RG_Hoare + Quote_Antiquote:
 
diff -r e0644528e21e -r 4bb592cdde0e src/HOL/HoareParallel/document/root.tex
--- a/src/HOL/HoareParallel/document/root.tex	Mon Apr 29 11:30:15 2002 +0200
+++ b/src/HOL/HoareParallel/document/root.tex	Mon Apr 29 16:45:12 2002 +0200
@@ -18,6 +18,26 @@
 \author{Leonor Prensa Nieto}
 \maketitle
 
+\begin{abstract}\noindent
+  In the following theories a formalization of the Owicki-Gries and
+  the rely-guarantee methods is presented. These methods are widely
+  used for correctness proofs of parallel imperative programs with
+  shared variables.  We define syntax, semantics and proof rules in
+  Isabelle/HOL.  The proof rules also provide for programs
+  parameterized in the number of parallel components. Their
+  correctness w.r.t.\ the semantics is proven.  Completeness proofs
+  for both methods are extended to the new case of parameterized
+  programs. (These proofs have not been formalized in Isabelle. They
+  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
+  verify several non-trivial examples for parameterized and
+  non-parameterized programs.  For the automatic generation of
+  verification conditions with the Owicki-Gries method we define a
+  tactic based on the proof rules.  The most involved examples are the
+  verification of two garbage-collection algorithms, the second one
+  parameterized in the number of mutators.
+
+\end{abstract}
+
 \pagestyle{plain}
 \thispagestyle{empty}
 \tableofcontents