--- a/src/HOL/IsaMakefile Thu Sep 22 16:30:47 2011 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 22 16:56:19 2011 +0200
@@ -68,6 +68,7 @@
HOL-Proofs-Lambda \
HOL-SET_Protocol \
HOL-SPARK-Examples \
+ HOL-SPARK-Manual \
HOL-Word-SMT_Examples \
HOL-Statespace \
TLA-Buffer \
@@ -1442,6 +1443,48 @@
@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Examples
+## HOL-SPARK-Manual
+
+HOL-SPARK-Manual: HOL-SPARK $(LOG)/HOL-SPARK-Manual.gz
+
+$(LOG)/HOL-SPARK-Manual.gz: $(OUT)/HOL-SPARK \
+ SPARK/Manual/ROOT.ML \
+ SPARK/Manual/Complex_Types.thy \
+ SPARK/Manual/Example_Verification.thy \
+ SPARK/Manual/Proc1.thy \
+ SPARK/Manual/Proc2.thy \
+ SPARK/Manual/Reference.thy \
+ SPARK/Manual/Simple_Greatest_Common_Divisor.thy \
+ SPARK/Manual/VC_Principles.thy \
+ SPARK/Manual/complex_types_app/initialize.fdl \
+ SPARK/Manual/complex_types_app/initialize.rls \
+ SPARK/Manual/complex_types_app/initialize.siv \
+ SPARK/Manual/loop_invariant/proc1.fdl \
+ SPARK/Manual/loop_invariant/proc1.rls \
+ SPARK/Manual/loop_invariant/proc1.siv \
+ SPARK/Manual/loop_invariant/proc2.fdl \
+ SPARK/Manual/loop_invariant/proc2.rls \
+ SPARK/Manual/loop_invariant/proc2.siv \
+ SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl \
+ SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls \
+ SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv \
+ SPARK/Manual/document/complex_types.ads \
+ SPARK/Manual/document/complex_types_app.adb \
+ SPARK/Manual/document/complex_types_app.ads \
+ SPARK/Manual/document/loop_invariant.adb \
+ SPARK/Manual/document/loop_invariant.ads \
+ SPARK/Manual/document/Simple_Gcd.adb \
+ SPARK/Manual/document/Simple_Gcd.ads \
+ SPARK/Manual/document/intro.tex \
+ SPARK/Manual/document/root.tex \
+ SPARK/Manual/document/root.bib \
+ SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \
+ SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \
+ SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \
+ SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv
+ @cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Manual
+
+
## HOL-Mutabelle
HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
@@ -1751,6 +1794,7 @@
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
+ $(LOG)/HOL-SPARK-Manual.gz \
$(LOG)/HOL-Statespace.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,114 @@
+theory Complex_Types
+imports SPARK
+begin
+
+datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
+
+record two_fields =
+ Field1 :: "int \<times> day \<Rightarrow> int"
+ Field2 :: int
+
+spark_types
+ complex_types__day = day
+ complex_types__record_type = two_fields
+
+definition
+ initialized3 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+ "initialized3 A i k = (\<forall>j\<in>{0..<k}. A (i, val j) = 0)"
+
+definition
+ initialized2 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> bool" where
+ "initialized2 A i = (\<forall>j\<in>{0..<i}. initialized3 A j 7)"
+
+definition
+ initialized :: "(int \<Rightarrow> two_fields) \<Rightarrow> int \<Rightarrow> bool" where
+ "initialized A i = (\<forall>j\<in>{0..<i}.
+ initialized2 (Field1 (A j)) 10 \<and> Field2 (A j) = 0)"
+
+spark_proof_functions
+ complex_types__initialized = initialized
+ complex_types__initialized2 = initialized2
+ complex_types__initialized3 = initialized3
+
+(*<*)
+spark_open "complex_types_app/initialize.siv"
+
+spark_vc procedure_initialize_1
+ by (simp add: initialized_def)
+
+spark_vc procedure_initialize_2
+proof -
+ from
+ `initialized a loop__1__i`
+ `initialized2 (Field1 (a loop__1__i)) 9`
+ `initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)`
+ show ?C1
+ apply (auto simp add: initialized_def initialized2_def initialized3_def)
+ apply (case_tac "j = 9")
+ apply auto
+ apply (case_tac "ja = 6")
+ apply auto
+ done
+ from H5
+ show ?C2 by simp
+qed
+
+spark_vc procedure_initialize_3
+ by (simp add: initialized2_def)
+
+spark_vc procedure_initialize_4
+proof -
+ from `initialized a loop__1__i`
+ show ?C1 by (simp add: initialized_def)
+ from
+ `initialized2 (Field1 (a loop__1__i)) loop__2__j`
+ `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)`
+ show ?C2
+ apply (auto simp add: initialized2_def initialized3_def)
+ apply (case_tac "j = loop__2__j")
+ apply auto
+ apply (case_tac "ja = 6")
+ apply auto
+ done
+ from H5
+ show ?C3 by simp
+qed
+
+spark_vc procedure_initialize_5
+ by (simp add: initialized3_def)
+
+spark_vc procedure_initialize_6
+proof -
+ from `initialized a loop__1__i`
+ show ?C1 by (simp add: initialized_def)
+ from `initialized2 (Field1 (a loop__1__i)) loop__2__j`
+ show ?C2 by (simp add: initialized2_def initialized3_def)
+ from
+ `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)`
+ `loop__3__k < Sun`
+ rangeI [of pos loop__3__k]
+ show ?C3
+ apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos)
+ apply (case_tac "j = pos loop__3__k")
+ apply (auto simp add: val_pos)
+ done
+ from H5
+ show ?C4 by simp
+qed
+
+spark_vc procedure_initialize_9
+ using
+ `initialized a 9`
+ `initialized2 (Field1 (a 9)) 9`
+ `initialized3 (Field1 (a 9)) 9 (pos Sun)`
+ apply (auto simp add: initialized_def initialized2_def initialized3_def)
+ apply (case_tac "j = 9")
+ apply auto
+ apply (case_tac "ja = 6")
+ apply auto
+ done
+
+spark_end
+(*>*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,250 @@
+(*<*)
+theory Example_Verification
+imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
+begin
+(*>*)
+
+chapter {* Verifying an Example Program *}
+
+text {*
+\label{sec:example-verification}
+\begin{figure}
+\lstinputlisting{Gcd.ads}
+\lstinputlisting{Gcd.adb}
+\caption{\SPARK{} program for computing the greatest common divisor}
+\label{fig:gcd-prog}
+\end{figure}
+
+\begin{figure}
+\input{Greatest_Common_Divisor}
+\caption{Correctness proof for the greatest common divisor program}
+\label{fig:gcd-proof}
+\end{figure}
+We will now explain the usage of the \SPARK{} verification environment by proving
+the correctness of an example program. As an example, we use a program for computing
+the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
+which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}.
+*}
+
+section {* Importing \SPARK{} VCs into Isabelle *}
+
+text {*
+In order to specify that the \SPARK{} procedure \texttt{G\_C\_D} behaves like its
+mathematical counterpart, Barnes introduces a \emph{proof function} \texttt{Gcd}
+in the package specification. Invoking the \SPARK{} Examiner and Simplifier on
+this program yields a file \texttt{g\_c\_d.siv} containing the simplified VCs,
+as well as files \texttt{g\_c\_d.fdl} and \texttt{g\_c\_d.rls}, containing FDL
+declarations and rules, respectively. The files generated by \SPARK{} are assumed to reside in the
+subdirectory \texttt{greatest\_common\_divisor}. For \texttt{G\_C\_D} the
+Examiner generates ten VCs, eight of which are proved automatically by
+the Simplifier. We now show how to prove the remaining two VCs
+interactively using HOL-\SPARK{}. For this purpose, we create a \emph{theory}
+\texttt{Greatest\_Common\_Divisor}, which is shown in \figref{fig:gcd-proof}.
+A theory file always starts with the keyword \isa{\isacommand{theory}} followed
+by the name of the theory, which must be the same as the file name. The theory
+name is followed by the keyword \isa{\isacommand{imports}} and a list of theories
+imported by the current theory. All theories using the HOL-\SPARK{} verification
+environment must import the theory \texttt{SPARK}. In addition, we also include
+the \texttt{GCD} theory. The list of imported theories is followed by the
+\isa{\isacommand{begin}} keyword. In order to interactively process the theory
+shown in \figref{fig:gcd-proof}, we start Isabelle with the command
+\begin{verbatim}
+ isabelle emacs -l HOL-SPARK Greatest_Common_Divisor.thy
+\end{verbatim}
+The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right
+object logic image containing the verification environment. Each proof function
+occurring in the specification of a \SPARK{} program must be linked with a
+corresponding Isabelle function. This is accomplished by the command
+\isa{\isacommand{spark\_proof\_functions}}, which expects a list of equations
+of the form \emph{name}\texttt{\ =\ }\emph{term}, where \emph{name} is the
+name of the proof function and \emph{term} is the corresponding Isabelle term.
+In the case of \texttt{gcd}, both the \SPARK{} proof function and its Isabelle
+counterpart happen to have the same name. Isabelle checks that the type of the
+term linked with a proof function agrees with the type of the function declared
+in the \texttt{*.fdl} file.
+It is worth noting that the
+\isa{\isacommand{spark\_proof\_functions}} command can be invoked both outside,
+i.e.\ before \isa{\isacommand{spark\_open}}, and inside the environment, i.e.\ after
+\isa{\isacommand{spark\_open}}, but before any \isa{\isacommand{spark\_vc}} command. The
+former variant is useful when having to declare proof functions that are shared by several
+procedures, whereas the latter has the advantage that the type of the proof function
+can be checked immediately, since the VCs, and hence also the declarations of proof
+functions in the \texttt{*.fdl} file have already been loaded.
+\begin{figure}
+\begin{flushleft}
+\tt
+Context: \\
+\ \\
+\begin{tabular}{ll}
+fixes & @{text "m ::"}\ "@{text int}" \\
+and & @{text "n ::"}\ "@{text int}" \\
+and & @{text "c ::"}\ "@{text int}" \\
+and & @{text "d ::"}\ "@{text int}" \\
+assumes & @{text "g_c_d_rules1:"}\ "@{text "0 \<le> integer__size"}" \\
+and & @{text "g_c_d_rules6:"}\ "@{text "0 \<le> natural__size"}" \\
+\multicolumn{2}{l}{notes definition} \\
+\multicolumn{2}{l}{\hspace{2ex}@{text "defns ="}\ `@{text "integer__first = - 2147483648"}`} \\
+\multicolumn{2}{l}{\hspace{4ex}`@{text "integer__last = 2147483647"}`} \\
+\multicolumn{2}{l}{\hspace{4ex}\dots}
+\end{tabular}\ \\[1.5ex]
+\ \\
+Definitions: \\
+\ \\
+\begin{tabular}{ll}
+@{text "g_c_d_rules2:"} & @{text "integer__first = - 2147483648"} \\
+@{text "g_c_d_rules3:"} & @{text "integer__last = 2147483647"} \\
+\dots
+\end{tabular}\ \\[1.5ex]
+\ \\
+Verification conditions: \\
+\ \\
+path(s) from assertion of line 10 to assertion of line 10 \\
+\ \\
+@{text procedure_g_c_d_4}\ (unproved) \\
+\ \ \begin{tabular}{ll}
+assumes & @{text "H1:"}\ "@{text "0 \<le> c"}" \\
+and & @{text "H2:"}\ "@{text "0 < d"}" \\
+and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\
+\dots \\
+shows & "@{text "0 < c - c sdiv d * d"}" \\
+and & "@{text "gcd d (c - c sdiv d * d) = gcd m n"}
+\end{tabular}\ \\[1.5ex]
+\ \\
+path(s) from assertion of line 10 to finish \\
+\ \\
+@{text procedure_g_c_d_11}\ (unproved) \\
+\ \ \begin{tabular}{ll}
+assumes & @{text "H1:"}\ "@{text "0 \<le> c"}" \\
+and & @{text "H2:"}\ "@{text "0 < d"}" \\
+and & @{text "H3:"}\ "@{text "gcd c d = gcd m n"}" \\
+\dots \\
+shows & "@{text "d = gcd m n"}"
+\end{tabular}
+\end{flushleft}
+\caption{Output of \isa{\isacommand{spark\_status}} for \texttt{g\_c\_d.siv}}
+\label{fig:gcd-status}
+\end{figure}
+We now instruct Isabelle to open
+a new verification environment and load a set of VCs. This is done using the
+command \isa{\isacommand{spark\_open}}, which must be given the name of a
+\texttt{*.siv} or \texttt{*.vcg} file as an argument. Behind the scenes, Isabelle
+parses this file and the corresponding \texttt{*.fdl} and \texttt{*.rls} files,
+and converts the VCs to Isabelle terms. Using the command \isa{\isacommand{spark\_status}},
+the user can display the current VCs together with their status (proved, unproved).
+The variants \isa{\isacommand{spark\_status}\ (proved)}
+and \isa{\isacommand{spark\_status}\ (unproved)} show only proved and unproved
+VCs, respectively. For \texttt{g\_c\_d.siv}, the output of
+\isa{\isacommand{spark\_status}} is shown in \figref{fig:gcd-status}.
+To minimize the number of assumptions, and hence the size of the VCs,
+FDL rules of the form ``\dots\ \texttt{may\_be\_replaced\_by}\ \dots'' are
+turned into native Isabelle definitions, whereas other rules are modelled
+as assumptions.
+*}
+
+section {* Proving the VCs *}
+
+text {*
+\label{sec:proving-vcs}
+The two open VCs are @{text procedure_g_c_d_4} and @{text procedure_g_c_d_11},
+both of which contain the @{text gcd} proof function that the \SPARK{} Simplifier
+does not know anything about. The proof of a particular VC can be started with
+the \isa{\isacommand{spark\_vc}} command, which is similar to the standard
+\isa{\isacommand{lemma}} and \isa{\isacommand{theorem}} commands, with the
+difference that it only takes a name of a VC but no formula as an argument.
+A VC can have several conclusions that can be referenced by the identifiers
+@{text "?C1"}, @{text "?C2"}, etc. If there is just one conclusion, it can
+also be referenced by @{text "?thesis"}. It is important to note that the
+\texttt{div} operator of FDL behaves differently from the @{text div} operator
+of Isabelle/HOL on negative numbers. The former always truncates towards zero,
+whereas the latter truncates towards minus infinity. This is why the FDL
+\texttt{div} operator is mapped to the @{text sdiv} operator in Isabelle/HOL,
+which is defined as
+@{thm [display] sdiv_def}
+For example, we have that
+@{lemma "-5 sdiv 4 = -1" by (simp add: sdiv_neg_pos)}, but
+@{lemma "(-5::int) div 4 = -2" by simp}.
+For non-negative dividend and divisor, @{text sdiv} is equivalent to @{text div},
+as witnessed by theorem @{text sdiv_pos_pos}:
+@{thm [display,mode=no_brackets] sdiv_pos_pos}
+In contrast, the behaviour of the FDL \texttt{mod} operator is equivalent to
+the one of Isabelle/HOL. Moreover, since FDL has no counterpart of the \SPARK{}
+operator \textbf{rem}, the \SPARK{} expression \texttt{c}\ \textbf{rem}\ \texttt{d}
+just becomes @{text "c - c sdiv d * d"} in Isabelle. The first conclusion of
+@{text procedure_g_c_d_4} requires us to prove that the remainder of @{text c}
+and @{text d} is greater than @{text 0}. To do this, we use the theorem
+@{text zmod_zdiv_equality'} describing the correspondence between @{text div}
+and @{text mod}
+@{thm [display] zmod_zdiv_equality'}
+together with the theorem @{text pos_mod_sign} saying that the result of the
+@{text mod} operator is non-negative when applied to a non-negative divisor:
+@{thm [display] pos_mod_sign}
+We will also need the aforementioned theorem @{text sdiv_pos_pos} in order for
+the standard Isabelle/HOL theorems about @{text div} to be applicable
+to the VC, which is formulated using @{text sdiv} rather that @{text div}.
+Note that the proof uses \texttt{`@{text "0 \<le> c"}`} and \texttt{`@{text "0 < d"}`}
+rather than @{text H1} and @{text H2} to refer to the hypotheses of the current
+VC. While the latter variant seems more compact, it is not particularly robust,
+since the numbering of hypotheses can easily change if the corresponding
+program is modified, making the proof script hard to adjust when there are many hypotheses.
+Moreover, proof scripts using abbreviations like @{text H1} and @{text H2}
+are hard to read without assistance from Isabelle.
+The second conclusion of @{text procedure_g_c_d_4} requires us to prove that
+the @{text gcd} of @{text d} and the remainder of @{text c} and @{text d}
+is equal to the @{text gcd} of the original input values @{text m} and @{text n},
+which is the actual \emph{invariant} of the procedure. This is a consequence
+of theorem @{text gcd_non_0_int}
+@{thm [display] gcd_non_0_int}
+Again, we also need theorems @{text zmod_zdiv_equality'} and @{text sdiv_pos_pos}
+to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
+@{text mod} operator for non-negative operands.
+The VC @{text procedure_g_c_d_11} says that if the loop invariant holds before
+the last iteration of the loop, the postcondition of the procedure will hold
+after execution of the loop body. To prove this, we observe that the remainder
+of @{text c} and @{text d}, and hence @{text "c mod d"} is @{text 0} when exiting
+the loop. This implies that @{text "gcd c d = d"}, since @{text c} is divisible
+by @{text d}, so the conclusion follows using the assumption @{text "gcd c d = gcd m n"}.
+This concludes the proofs of the open VCs, and hence the \SPARK{} verification
+environment can be closed using the command \isa{\isacommand{spark\_end}}.
+This command checks that all VCs have been proved and issues an error message
+if there are remaining unproved VCs. Moreover, Isabelle checks that there is
+no open \SPARK{} verification environment when the final \isa{\isacommand{end}}
+command of a theory is encountered.
+*}
+
+section {* Optimizing the proof *}
+
+text {*
+\begin{figure}
+\lstinputlisting{Simple_Gcd.adb}
+\input{Simple_Greatest_Common_Divisor}
+\caption{Simplified greatest common divisor program and proof}
+\label{fig:simple-gcd-proof}
+\end{figure}
+When looking at the program from \figref{fig:gcd-prog} once again, several
+optimizations come to mind. First of all, like the input parameters of the
+procedure, the local variables \texttt{C}, \texttt{D}, and \texttt{R} can
+be declared as \texttt{Natural} rather than \texttt{Integer}. Since natural
+numbers are non-negative by construction, the values computed by the algorithm
+are trivially proved to be non-negative. Since we are working with non-negative
+numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
+\textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'}
+and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{Barnes},
+we can simplify matters by placing the \textbf{assert} statement between
+\textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
+In the former case, the loop invariant has to be proved only once, whereas in
+the latter case, it has to be proved twice: since the \textbf{assert} occurs after
+the check of the exit condition, the invariant has to be proved for the path
+from the \textbf{assert} statement to the \textbf{assert} statement, and for
+the path from the \textbf{assert} statement to the postcondition. In the case
+of the \texttt{G\_C\_D} procedure, this might not seem particularly problematic,
+since the proof of the invariant is very simple, but it can unnecessarily
+complicate matters if the proof of the invariant is non-trivial. The simplified
+program for computing the greatest common divisor, together with its correctness
+proof, is shown in \figref{fig:simple-gcd-proof}. Since the package specification
+has not changed, we only show the body of the packages. The two VCs can now be
+proved by a single application of Isabelle's proof method @{text simp}.
+*}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Proc1.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,18 @@
+theory Proc1
+imports SPARK
+begin
+
+spark_open "loop_invariant/proc1.siv"
+
+spark_vc procedure_proc1_5
+ by (simp add: ring_distribs pull_mods)
+
+spark_vc procedure_proc1_8
+ by (simp add: ring_distribs pull_mods)
+
+spark_end
+
+lemma pow_2_32_simp: "4294967296 = (2::int)^32"
+ by simp
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Proc2.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,12 @@
+theory Proc2
+imports SPARK
+begin
+
+spark_open "loop_invariant/proc2.siv"
+
+spark_vc procedure_proc2_7
+ by (simp add: ring_distribs pull_mods)
+
+spark_end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/ROOT.ML Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,7 @@
+Printer.show_question_marks_default := false;
+
+use_thys
+ ["Example_Verification",
+ "VC_Principles",
+ "Reference",
+ "Complex_Types"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Reference.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,309 @@
+(*<*)
+theory Reference
+imports SPARK
+begin
+
+syntax (my_constrain output)
+ "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
+(*>*)
+
+chapter {* HOL-\SPARK{} Reference *}
+
+text {*
+\label{sec:spark-reference}
+This section is intended as a quick reference for the HOL-\SPARK{} verification
+environment. In \secref{sec:spark-commands}, we give a summary of the commands
+provided by the HOL-\SPARK{}, while \secref{sec:spark-types} contains a description
+of how particular types of \SPARK{} and FDL are modelled in Isabelle.
+*}
+
+section {* Commands *}
+
+text {*
+\label{sec:spark-commands}
+This section describes the syntax and effect of each of the commands provided
+by HOL-\SPARK{}.
+@{rail "@'spark_open' name ('(' name ')')?"}
+Opens a new \SPARK{} verification environment and loads a file with VCs. The file can be either
+a \texttt{*.vcg} or a \texttt{*.siv} file. The corresponding \texttt{*.fdl} and \texttt{*.rls}
+files must reside in the same directory as the file given as an argument to the command.
+This command also generates records and datatypes for the types specified in the
+\texttt{*.fdl} file, unless they have already been associated with user-defined
+Isabelle types (see below).
+Since the full package name currently cannot be determined from the files generated by the
+\SPARK{} Examiner, the command also allows to specify an optional package prefix in the
+format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
+packages, this is necessary in order for the verification environment to be able to map proof
+functions and types defined in Isabelle to their \SPARK{} counterparts.
+@{rail "@'spark_proof_functions' ((name '=' term)+)"}
+Associates a proof function with the given name to a term. The name should be the full name
+of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
+This command can be used both inside and outside a verification environment. The latter
+variant is useful for introducing proof functions that are shared by several procedures
+or packages, whereas the former allows the given term to refer to the types generated
+by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
+\texttt{*.fdl} file.
+@{rail "@'spark_types' ((name '=' type)+)"}
+Associates a \SPARK{} type with the given name with an Isabelle type. This command can
+only be used outside a verification environment. The given type must be either a record
+or a datatype, where the field names and constructors must match those of the corresponding
+\SPARK{} types (modulo casing). This command is useful when having to define
+proof functions referring to record or enumeration types that are shared by several
+procedures or packages. First, the types required by the proof functions can be introduced
+using Isabelle's commands for defining records or datatypes. Having introduced the
+types, the proof functions can be defined in Isabelle. Finally, both the proof
+functions and the types can be associated with their \SPARK{} counterparts.
+@{rail "@'spark_status' (('(proved)' | '(unproved)')?)"}
+Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
+the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
+The output can be restricted to the proved or unproved VCs by giving the corresponding
+option to the command.
+@{rail "@'spark_vc' name"}
+Initiates the proof of the VC with the given name. Similar to the standard
+\isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
+must be followed by a sequence of proof commands. The command introduces the
+hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
+\texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
+@{rail "@'spark_end'"}
+Closes the current verification environment. All VCs must have been proved,
+otherwise the command issues an error message. As a side effect, the command
+generates a proof review (\texttt{*.prv}) file to inform POGS of the proved
+VCs.
+*}
+
+section {* Types *}
+
+text {*
+\label{sec:spark-types}
+The main types of FDL are integers, enumeration types, records, and arrays.
+In the following sections, we describe how these types are modelled in
+Isabelle.
+*}
+
+subsection {* Integers *}
+
+text {*
+The FDL type \texttt{integer} is modelled by the Isabelle type @{typ int}.
+While the FDL \texttt{mod} operator behaves in the same way as its Isabelle
+counterpart, this is not the case for the \texttt{div} operator. As has already
+been mentioned in \secref{sec:proving-vcs}, the \texttt{div} operator of \SPARK{}
+always truncates towards zero, whereas the @{text div} operator of Isabelle
+truncates towards minus infinity. Therefore, the FDL \texttt{div} operator is
+mapped to the @{text sdiv} operator in Isabelle. The characteristic theorems
+of @{text sdiv}, in particular those describing the relationship with the standard
+@{text div} operator, are shown in \figref{fig:sdiv-properties}
+\begin{figure}
+\begin{center}
+\small
+\begin{tabular}{ll}
+@{text sdiv_def}: & @{thm sdiv_def} \\
+@{text sdiv_minus_dividend}: & @{thm sdiv_minus_dividend} \\
+@{text sdiv_minus_divisor}: & @{thm sdiv_minus_divisor} \\
+@{text sdiv_pos_pos}: & @{thm [mode=no_brackets] sdiv_pos_pos} \\
+@{text sdiv_pos_neg}: & @{thm [mode=no_brackets] sdiv_pos_neg} \\
+@{text sdiv_neg_pos}: & @{thm [mode=no_brackets] sdiv_neg_pos} \\
+@{text sdiv_neg_neg}: & @{thm [mode=no_brackets] sdiv_neg_neg} \\
+\end{tabular}
+\end{center}
+\caption{Characteristic properties of @{text sdiv}}
+\label{fig:sdiv-properties}
+\end{figure}
+
+\begin{figure}
+\begin{center}
+\small
+\begin{tabular}{ll}
+@{text AND_lower}: & @{thm [mode=no_brackets] AND_lower} \\
+@{text OR_lower}: & @{thm [mode=no_brackets] OR_lower} \\
+@{text XOR_lower}: & @{thm [mode=no_brackets] XOR_lower} \\
+@{text AND_upper1}: & @{thm [mode=no_brackets] AND_upper1} \\
+@{text AND_upper2}: & @{thm [mode=no_brackets] AND_upper2} \\
+@{text OR_upper}: & @{thm [mode=no_brackets] OR_upper} \\
+@{text XOR_upper}: & @{thm [mode=no_brackets] XOR_upper} \\
+@{text AND_mod}: & @{thm [mode=no_brackets] AND_mod}
+\end{tabular}
+\end{center}
+\caption{Characteristic properties of bitwise operators}
+\label{fig:bitwise}
+\end{figure}
+The bitwise logical operators of \SPARK{} and FDL are modelled by the operators
+@{text AND}, @{text OR} and @{text XOR} from Isabelle's @{text Word} library,
+all of which have type @{typ "int \<Rightarrow> int \<Rightarrow> int"}. A list of properties of these
+operators that are useful in proofs about \SPARK{} programs are shown in
+\figref{fig:bitwise}
+*}
+
+subsection {* Enumeration types *}
+
+text {*
+The FDL enumeration type
+\begin{alltt}
+type \(t\) = (\(e\sb{1}\), \(e\sb{2}\), \dots, \(e\sb{n}\));
+\end{alltt}
+is modelled by the Isabelle datatype
+\begin{isabelle}
+\normalsize
+\isacommand{datatype}\ $t$\ =\ $e_1$\ $\mid$\ $e_2$\ $\mid$\ \dots\ $\mid$\ $e_n$
+\end{isabelle}
+The HOL-\SPARK{} environment defines a type class @{class spark_enum} that captures
+the characteristic properties of all enumeration types. It provides the following
+polymorphic functions and constants for all types @{text "'a"} of this type class:
+\begin{flushleft}
+@{term_type [mode=my_constrain] pos} \\
+@{term_type [mode=my_constrain] val} \\
+@{term_type [mode=my_constrain] succ} \\
+@{term_type [mode=my_constrain] pred} \\
+@{term_type [mode=my_constrain] first_el} \\
+@{term_type [mode=my_constrain] last_el}
+\end{flushleft}
+In addition, @{class spark_enum} is a subclass of the @{class linorder} type class,
+which allows the comparison operators @{text "<"} and @{text "\<le>"} to be used on
+enumeration types. The polymorphic operations shown above enjoy a number of
+generic properties that hold for all enumeration types. These properties are
+listed in \figref{fig:enum-generic-properties}.
+Moreover, \figref{fig:enum-specific-properties} shows a list of properties
+that are specific to each enumeration type $t$, such as the characteristic
+equations for @{term val} and @{term pos}.
+\begin{figure}[t]
+\begin{center}
+\small
+\begin{tabular}{ll}
+@{text range_pos}: & @{thm range_pos} \\
+@{text less_pos}: & @{thm less_pos} \\
+@{text less_eq_pos}: & @{thm less_eq_pos} \\
+@{text val_def}: & @{thm val_def} \\
+@{text succ_def}: & @{thm succ_def} \\
+@{text pred_def}: & @{thm pred_def} \\
+@{text first_el_def}: & @{thm first_el_def} \\
+@{text last_el_def}: & @{thm last_el_def} \\
+@{text inj_pos}: & @{thm inj_pos} \\
+@{text val_pos}: & @{thm val_pos} \\
+@{text pos_val}: & @{thm pos_val} \\
+@{text first_el_smallest}: & @{thm first_el_smallest} \\
+@{text last_el_greatest}: & @{thm last_el_greatest} \\
+@{text pos_succ}: & @{thm pos_succ} \\
+@{text pos_pred}: & @{thm pos_pred} \\
+@{text succ_val}: & @{thm succ_val} \\
+@{text pred_val}: & @{thm pred_val}
+\end{tabular}
+\end{center}
+\caption{Generic properties of functions on enumeration types}
+\label{fig:enum-generic-properties}
+\end{figure}
+\begin{figure}[t]
+\begin{center}
+\small
+\begin{tabular}{ll@ {\hspace{2cm}}ll}
+\texttt{$t$\_val}: & \isa{val\ $0$\ =\ $e_1$} & \texttt{$t$\_pos}: & pos\ $e_1$\ =\ $0$ \\
+ & \isa{val\ $1$\ =\ $e_2$} & & pos\ $e_2$\ =\ $1$ \\
+ & \hspace{1cm}\vdots & & \hspace{1cm}\vdots \\
+ & \isa{val\ $(n-1)$\ =\ $e_n$} & & pos\ $e_n$\ =\ $n-1$
+\end{tabular} \\[3ex]
+\begin{tabular}{ll}
+\texttt{$t$\_card}: & \isa{card($t$)\ =\ $n$} \\
+\texttt{$t$\_first\_el}: & \isa{first\_el\ =\ $e_1$} \\
+\texttt{$t$\_last\_el}: & \isa{last\_el\ =\ $e_n$}
+\end{tabular}
+\end{center}
+\caption{Type-specific properties of functions on enumeration types}
+\label{fig:enum-specific-properties}
+\end{figure}
+*}
+
+subsection {* Records *}
+
+text {*
+The FDL record type
+\begin{alltt}
+type \(t\) = record
+ \(f\sb{1}\) : \(t\sb{1}\);
+ \(\vdots\)
+ \(f\sb{n}\) : \(t\sb{n}\)
+ end;
+\end{alltt}
+is modelled by the Isabelle record type
+\begin{isabelle}
+\normalsize
+\isacommand{record}\ t\ = \isanewline
+\ \ $f_1$\ ::\ $t_1$ \isanewline
+\ \ \ \vdots \isanewline
+\ \ $f_n$\ ::\ $t_n$
+\end{isabelle}
+Records are constructed using the notation
+\isa{\isasymlparr$f_1$\ =\ $v_1$,\ $\ldots$,\ $f_n$\ =\ $v_n$\isasymrparr},
+a field $f_i$ of a record $r$ is selected using the notation $f_i~r$, and the
+fields $f$ and $f'$ of a record $r$ can be updated using the notation
+\mbox{\isa{$r$\ \isasymlparr$f$\ :=\ $v$,\ $f'$\ :=\ $v'$\isasymrparr}}.
+*}
+
+subsection {* Arrays *}
+
+text {*
+The FDL array type
+\begin{alltt}
+type \(t\) = array [\(t\sb{1}\), \(\ldots\), \(t\sb{n}\)] of \(u\);
+\end{alltt}
+is modelled by the Isabelle function type $t_1 \times \cdots \times t_n \Rightarrow u$.
+Array updates are written as \isa{$A$($x_1$\ := $y_1$,\ \dots,\ $x_n$\ :=\ $y_n$)}.
+To allow updating an array at a set of indices, HOL-\SPARK{} provides the notation
+\isa{\dots\ [:=]\ \dots}, which can be combined with \isa{\dots\ :=\ \dots} and has
+the properties
+@{thm [display,mode=no_brackets] fun_upds_in fun_upds_notin upds_singleton}
+Thus, we can write expressions like
+@{term [display] "(A::int\<Rightarrow>int) ({0..9} [:=] 42, 15 := 99, {20..29} [:=] 0)"}
+that would be cumbersome to write using single updates.
+*}
+
+section {* User-defined proof functions and types *}
+
+text {*
+To illustrate the interplay between the commands for introducing user-defined proof
+functions and types mentioned in \secref{sec:spark-commands}, we now discuss a larger
+example involving the definition of proof functions on complex types. Assume we would
+like to define an array type, whose elements are records that themselves contain
+arrays. Moreover, assume we would like to initialize all array elements and record
+fields of type \texttt{Integer} in an array of this type with the value \texttt{0}.
+The specification of package \texttt{Complex\_Types} containing the definition of
+the array type, which we call \texttt{Array\_Type2}, is shown in \figref{fig:complex-types}.
+It also contains the declaration of a proof function \texttt{Initialized} that is used
+to express that the array has been initialized. The two other proof functions
+\texttt{Initialized2} and \texttt{Initialized3} are used to reason about the
+initialization of the inner array. Since the array types and proof functions
+may be used by several packages, such as the one shown in \figref{fig:complex-types-app},
+it is advantageous to define the proof functions in a central theory that can
+be included by other theories containing proofs about packages using \texttt{Complex\_Types}.
+We show this theory in \figref{fig:complex-types-thy}. Since the proof functions
+refer to the enumeration and record types defined in \texttt{Complex\_Types},
+we need to define the Isabelle counterparts of these types using the
+\isa{\isacommand{datatype}} and \isa{\isacommand{record}} commands in order
+to be able to write down the definition of the proof functions. These types are
+linked to the corresponding \SPARK{} types using the \isa{\isacommand{spark\_types}}
+command. Note that we have to specify the full name of the \SPARK{} functions
+including the package prefix. Using the logic of Isabelle, we can then define
+functions involving the enumeration and record types introduced above, and link
+them to the corresponding \SPARK{} proof functions. It is important that the
+\isa{\isacommand{definition}} commands are preceeded by the \isa{\isacommand{spark\_types}}
+command, since the definition of @{text initialized3} uses the @{text val}
+function for enumeration types that is only available once that @{text day}
+has been declared as a \SPARK{} type.
+\begin{figure}
+\lstinputlisting{complex_types.ads}
+\caption{Nested array and record types}
+\label{fig:complex-types}
+\end{figure}
+\begin{figure}
+\lstinputlisting{complex_types_app.ads}
+\lstinputlisting{complex_types_app.adb}
+\caption{Application of \texttt{Complex\_Types} package}
+\label{fig:complex-types-app}
+\end{figure}
+\begin{figure}
+\input{Complex_Types}
+\caption{Theory defining proof functions for complex types}
+\label{fig:complex-types-thy}
+\end{figure}
+*}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
+ Author: Stefan Berghofer
+ Copyright: secunet Security Networks AG
+*)
+
+theory Simple_Greatest_Common_Divisor
+imports SPARK GCD
+begin
+
+spark_proof_functions
+ gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
+
+spark_open "simple_greatest_common_divisor/g_c_d.siv"
+
+spark_vc procedure_g_c_d_4
+ using `0 < d` `gcd c d = gcd m n`
+ by (simp add: gcd_non_0_int)
+
+spark_vc procedure_g_c_d_9
+ using `0 \<le> c` `gcd c 0 = gcd m n`
+ by simp
+
+spark_end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,152 @@
+(*<*)
+theory VC_Principles
+imports Proc1 Proc2
+begin
+(*>*)
+
+chapter {* Principles of VC generation *}
+
+text {*
+\label{sec:vc-principles}
+In this section, we will discuss some aspects of VC generation that are
+useful for understanding and optimizing the VCs produced by the \SPARK{}
+Examiner.
+
+\begin{figure}
+\lstinputlisting{loop_invariant.ads}
+\lstinputlisting{loop_invariant.adb}
+\caption{Assertions in for-loops}
+\label{fig:loop-invariant-ex}
+\end{figure}
+\begin{figure}
+\begin{tikzpicture}
+\tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
+\node[box] (pre) at (0,0) {precondition};
+\node[box] (assn) at (0,-3) {assertion};
+\node[box] (post) at (0,-6) {postcondition};
+\draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn);
+\draw[-latex] (assn) .. controls (2.5,-4.5) and (2.5,-1.5) .. %
+node [right] {\small$\begin{array}{l} %
+(i - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
+(i + 1 - 1) * b \mod 2^{32} ~= \\ %
+(c + b) \mod 2^{32} %
+\end{array}$} (assn);
+\draw[-latex] (assn) -- node [right] {\small$\begin{array}{l} %
+(a - 1) * b \mod 2^{32} = c ~\longrightarrow \\ %
+a * b \mod 2^{32} = (c + b) \mod 2^{32} %
+\end{array}$} (post);
+\draw[-latex] (pre) .. controls (-2,-3) .. %
+node [left] {\small$\begin{array}{l} %
+\neg 1 \le a ~\longrightarrow \\ %
+a * b \mod 2^{32} = 0 %
+\end{array}$} (post);
+\end{tikzpicture}
+\caption{Control flow graph for procedure \texttt{Proc1}}
+\label{fig:proc1-graph}
+\end{figure}
+\begin{figure}
+\begin{tikzpicture}
+\tikzstyle{box}=[draw, drop shadow, fill=white, rounded corners]
+\node[box] (pre) at (0,0) {precondition};
+\node[box] (assn1) at (2,-3) {assertion 1};
+\node[box] (assn2) at (2,-6) {assertion 2};
+\node[box] (post) at (0,-9) {postcondition};
+\draw[-latex] (pre) -- node [right] {\small$(1 - 1) * b \mod 2^{32} = 0$} (assn1);
+\draw[-latex] (assn1) -- node [left] {\small$\begin{array}{l} %
+(i - 1) * b \mod 2^{32} = c \\ %
+\longrightarrow \\ %
+i * b \mod 2^{32} = \\ %
+(c + b) \mod 2^{32} %
+\end{array}$} (assn2);
+\draw[-latex] (assn2) .. controls (4.5,-7.5) and (4.5,-1.5) .. %
+node [right] {\small$\begin{array}{l} %
+i * b \mod 2^{32} = c ~\longrightarrow \\ %
+(i + 1 - 1) * b \mod 2^{32} = c %
+\end{array}$} (assn1);
+\draw[-latex] (assn2) -- node [right] {\small$\begin{array}{l} %
+a * b \mod 2^{32} = c ~\longrightarrow \\ %
+a * b \mod 2^{32} = c %
+\end{array}$} (post);
+\draw[-latex] (pre) .. controls (-3,-3) and (-3,-6) .. %
+node [left,very near start] {\small$\begin{array}{l} %
+\neg 1 \le a ~\longrightarrow \\ %
+a * b \mod 2^{32} = 0 %
+\end{array}$} (post);
+\end{tikzpicture}
+\caption{Control flow graph for procedure \texttt{Proc2}}
+\label{fig:proc2-graph}
+\end{figure}
+As explained by Barnes \cite[\S 11.5]{Barnes}, the \SPARK{} Examiner unfolds the loop
+\begin{lstlisting}
+for I in T range L .. U loop
+ --# assert P (I);
+ S;
+end loop;
+\end{lstlisting}
+to
+\begin{lstlisting}
+if L <= U then
+ I := L;
+ loop
+ --# assert P (I);
+ S;
+ exit when I = U;
+ I := I + 1;
+ end loop;
+end if;
+\end{lstlisting}
+Due to this treatment of for-loops, the user essentially has to prove twice that
+\texttt{S} preserves the invariant \textit{\texttt{P}}, namely for
+the path from the assertion to the assertion and from the assertion to the next cut
+point following the loop. The preservation of the invariant has to be proved even
+more often when the loop is followed by an if-statement. For trivial invariants,
+this might not seem like a big problem, but in realistic applications, where invariants
+are complex, this can be a major inconvenience. Often, the proofs of the invariant differ
+only in a few variables, so it is tempting to just copy and modify existing proof scripts,
+but this leads to proofs that are hard to maintain.
+The problem of having to prove the invariant several times can be avoided by rephrasing
+the above for-loop to
+\begin{lstlisting}
+for I in T range L .. U loop
+ --# assert P (I);
+ S;
+ --# assert P (I + 1)
+end loop;
+\end{lstlisting}
+The VC for the path from the second assertion to the first assertion is trivial and can
+usually be proved automatically by the \SPARK{} Simplifier, whereas the VC for the path
+from the first assertion to the second assertion actually expresses the fact that
+\texttt{S} preserves the invariant.
+
+We illustrate this technique using the example package shown in \figref{fig:loop-invariant-ex}.
+It contains two procedures \texttt{Proc1} and \texttt{Proc2}, both of which implement
+multiplication via addition. The procedures have the same specification, but in \texttt{Proc1},
+only one \textbf{assert} statement is placed at the beginning of the loop, whereas \texttt{Proc2}
+employs the trick explained above.
+After applying the \SPARK{} Simplifier to the VCs generated for \texttt{Proc1}, two very
+similar VCs
+@{thm [display] (concl) procedure_proc1_5 [simplified pow_2_32_simp]}
+and
+@{thm [display,margin=60] (concl) procedure_proc1_8 [simplified pow_2_32_simp]}
+remain, whereas for \texttt{Proc2}, only the first of the above VCs remains.
+Why placing \textbf{assert} statements both at the beginning and at the end of the loop body
+simplifies the proof of the invariant should become obvious when looking at \figref{fig:proc1-graph}
+and \figref{fig:proc2-graph} showing the \emph{control flow graphs} for \texttt{Proc1} and
+\texttt{Proc2}, respectively. The nodes in the graph correspond to cut points in the program,
+and the paths between the cut points are annotated with the corresponding VCs. To reduce the
+size of the graphs, we do not show nodes and edges corresponding to runtime checks.
+The VCs for the path bypassing the loop and for the path from the precondition to the
+(first) assertion are the same for both procedures. The graph for \texttt{Proc1} contains
+two VCs expressing that the invariant is preserved by the execution of the loop body: one
+for the path from the assertion to the assertion, and another one for the path from the
+assertion to the conclusion, which corresponds to the last iteration of the loop. The latter
+VC can be obtained from the former by simply replacing $i$ by $a$. In contrast, the graph
+for \texttt{Proc2} contains only one such VC for the path from assertion 1 to assertion 2.
+The VC for the path from assertion 2 to assertion 1 is trivial, and so is the VC for the
+path from assertion 2 to the postcondition, expressing that the loop invariant implies
+the postcondition when the loop has terminated.
+*}
+
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/complex_types_app/initialize.fdl Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,52 @@
+ {*******************************************************}
+ {FDL Declarations}
+ {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039}
+ {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.}
+ {*******************************************************}
+
+
+ {DATE : 22-SEP-2011 11:10:52.42}
+
+ {procedure Complex_Types_App.Initialize}
+
+
+title procedure initialize;
+
+ function round__(real) : integer;
+ type complex_types__day = (complex_types__mon,
+ complex_types__tue, complex_types__wed, complex_types__thu,
+ complex_types__fri, complex_types__sat, complex_types__sun);
+ type complex_types__array_type1 = array [integer,
+ complex_types__day] of integer;
+ type complex_types__record_type = record
+ field1 : complex_types__array_type1;
+ field2 : integer
+ end;
+ type complex_types__array_type2 = array [integer] of
+ complex_types__record_type;
+ const complex_types__array_index__base__first : integer = pending;
+ const complex_types__array_index__base__last : integer = pending;
+ const complex_types__day__base__first : complex_types__day = pending;
+ const complex_types__day__base__last : complex_types__day = pending;
+ const integer__base__first : integer = pending;
+ const integer__base__last : integer = pending;
+ const complex_types__record_type__size : integer = pending;
+ const complex_types__array_index__first : integer = pending;
+ const complex_types__array_index__last : integer = pending;
+ const complex_types__array_index__size : integer = pending;
+ const complex_types__day__first : complex_types__day = pending;
+ const complex_types__day__last : complex_types__day = pending;
+ function complex_types__day__pos(complex_types__day) : integer;
+ const complex_types__day__size : integer = pending;
+ const integer__first : integer = pending;
+ const integer__last : integer = pending;
+ const integer__size : integer = pending;
+ var a : complex_types__array_type2;
+ var loop__1__i : integer;
+ var loop__2__j : integer;
+ var loop__3__k : complex_types__day;
+ function complex_types__initialized(complex_types__array_type2, integer) : boolean;
+ function complex_types__initialized2(complex_types__array_type1, integer) : boolean;
+ function complex_types__initialized3(complex_types__array_type1, integer, integer) : boolean;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/complex_types_app/initialize.rls Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,94 @@
+ /*********************************************************/
+ /*Proof Rule Declarations*/
+ /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
+ /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
+ /*********************************************************/
+
+
+ /*DATE : 22-SEP-2011 11:10:52.42*/
+
+ /*procedure Complex_Types_App.Initialize*/
+
+
+rule_family initialize_rules:
+ X requires [X:any] &
+ X <= Y requires [X:ire, Y:ire] &
+ X >= Y requires [X:ire, Y:ire].
+
+initialize_rules(1): integer__size >= 0 may_be_deduced.
+initialize_rules(2): integer__first may_be_replaced_by -2147483648.
+initialize_rules(3): integer__last may_be_replaced_by 2147483647.
+initialize_rules(4): integer__base__first may_be_replaced_by -2147483648.
+initialize_rules(5): integer__base__last may_be_replaced_by 2147483647.
+initialize_rules(6): complex_types__day__size >= 0 may_be_deduced.
+initialize_rules(7): complex_types__day__first may_be_replaced_by complex_types__mon.
+initialize_rules(8): complex_types__day__last may_be_replaced_by complex_types__sun.
+initialize_rules(9): complex_types__day__base__first may_be_replaced_by complex_types__mon.
+initialize_rules(10): complex_types__day__base__last may_be_replaced_by complex_types__sun.
+initialize_rules(11): complex_types__day__pos(complex_types__day__first) may_be_replaced_by 0.
+initialize_rules(12): complex_types__day__pos(complex_types__mon) may_be_replaced_by 0.
+initialize_rules(13): complex_types__day__val(0) may_be_replaced_by
+ complex_types__mon.
+initialize_rules(14): complex_types__day__pos(complex_types__tue) may_be_replaced_by 1.
+initialize_rules(15): complex_types__day__val(1) may_be_replaced_by
+ complex_types__tue.
+initialize_rules(16): complex_types__day__pos(complex_types__wed) may_be_replaced_by 2.
+initialize_rules(17): complex_types__day__val(2) may_be_replaced_by
+ complex_types__wed.
+initialize_rules(18): complex_types__day__pos(complex_types__thu) may_be_replaced_by 3.
+initialize_rules(19): complex_types__day__val(3) may_be_replaced_by
+ complex_types__thu.
+initialize_rules(20): complex_types__day__pos(complex_types__fri) may_be_replaced_by 4.
+initialize_rules(21): complex_types__day__val(4) may_be_replaced_by
+ complex_types__fri.
+initialize_rules(22): complex_types__day__pos(complex_types__sat) may_be_replaced_by 5.
+initialize_rules(23): complex_types__day__val(5) may_be_replaced_by
+ complex_types__sat.
+initialize_rules(24): complex_types__day__pos(complex_types__sun) may_be_replaced_by 6.
+initialize_rules(25): complex_types__day__val(6) may_be_replaced_by
+ complex_types__sun.
+initialize_rules(26): complex_types__day__pos(complex_types__day__last) may_be_replaced_by 6.
+initialize_rules(27): complex_types__day__pos(succ(X)) may_be_replaced_by
+ complex_types__day__pos(X) + 1
+ if [X <=complex_types__sun, X <> complex_types__sun].
+initialize_rules(28): complex_types__day__pos(pred(X)) may_be_replaced_by
+ complex_types__day__pos(X) - 1
+ if [X >=complex_types__mon, X <> complex_types__mon].
+initialize_rules(29): complex_types__day__pos(X) >= 0 may_be_deduced_from
+ [complex_types__mon <= X, X <= complex_types__sun].
+initialize_rules(30): complex_types__day__pos(X) <= 6 may_be_deduced_from
+ [complex_types__mon <= X, X <= complex_types__sun].
+initialize_rules(31): complex_types__day__val(X) >=
+ complex_types__mon may_be_deduced_from
+ [0 <= X, X <= 6].
+initialize_rules(32): complex_types__day__val(X) <=
+ complex_types__sun may_be_deduced_from
+ [0 <= X, X <= 6].
+initialize_rules(33): succ(complex_types__day__val(X)) may_be_replaced_by
+ complex_types__day__val(X+1)
+ if [0 <= X, X < 6].
+initialize_rules(34): pred(complex_types__day__val(X)) may_be_replaced_by
+ complex_types__day__val(X-1)
+ if [0 < X, X <= 6].
+initialize_rules(35): complex_types__day__pos(complex_types__day__val(X)) may_be_replaced_by X
+ if [0 <= X, X <= 6].
+initialize_rules(36): complex_types__day__val(complex_types__day__pos(X)) may_be_replaced_by X
+ if [complex_types__mon <= X, X <= complex_types__sun].
+initialize_rules(37): complex_types__day__pos(X) <=
+ complex_types__day__pos(Y) & X <= Y are_interchangeable
+ if [complex_types__mon <= X, X <= complex_types__sun,
+ complex_types__mon <= Y, Y <= complex_types__sun].
+initialize_rules(38): complex_types__day__val(X) <=
+ complex_types__day__val(Y) & X <= Y are_interchangeable
+ if [0 <= X, X <= 6, 0 <= Y, Y <= 6].
+initialize_rules(39): complex_types__array_index__size >= 0 may_be_deduced.
+initialize_rules(40): complex_types__array_index__first may_be_replaced_by 0.
+initialize_rules(41): complex_types__array_index__last may_be_replaced_by 9.
+initialize_rules(42): complex_types__array_index__base__first may_be_replaced_by -2147483648.
+initialize_rules(43): complex_types__array_index__base__last may_be_replaced_by 2147483647.
+initialize_rules(44): complex_types__record_type__size >= 0 may_be_deduced.
+initialize_rules(45): A = B may_be_deduced_from
+ [goal(checktype(A,complex_types__record_type)),
+ goal(checktype(B,complex_types__record_type)),
+ fld_field1(A) = fld_field1(B),
+ fld_field2(A) = fld_field2(B)].
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/complex_types_app/initialize.siv Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,257 @@
+*****************************************************************************
+ Semantic Analysis of SPARK Text
+ Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+ Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+*****************************************************************************
+
+
+CREATED 22-SEP-2011, 11:10:52 SIMPLIFIED 22-SEP-2011, 11:10:53
+
+SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+
+procedure Complex_Types_App.Initialize
+
+
+
+
+For path(s) from start to assertion of line 7:
+
+procedure_initialize_1.
+H1: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H3: integer__size >= 0 .
+H4: complex_types__day__size >= 0 .
+H5: complex_types__array_index__size >= 0 .
+H6: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized(a, 0) .
+
+
+For path(s) from assertion of line 15 to assertion of line 7:
+
+procedure_initialize_2.
+H1: complex_types__initialized(a, loop__1__i) .
+H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 9) .
+H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])), 9,
+ complex_types__day__pos(complex_types__sun)) .
+H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H6: loop__1__i >= 0 .
+H7: loop__1__i < 9 .
+H8: integer__size >= 0 .
+H9: complex_types__day__size >= 0 .
+H10: complex_types__array_index__size >= 0 .
+H11: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(upf_field2(
+ element(a, [loop__1__i]), 0), update(fld_field1(element(a, [
+ loop__1__i])), [9, complex_types__sun], 0))), loop__1__i + 1) .
+C2: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1(
+ element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [
+ i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(upf_field2(element(a, [loop__1__i]), 0), update(fld_field1(
+ element(a, [loop__1__i])), [9, complex_types__sun], 0))), [i___1])), [
+ i___2, i___3]) <= 2147483647))) .
+
+
+For path(s) from assertion of line 7 to assertion of line 10:
+
+procedure_initialize_3.
+H1: complex_types__initialized(a, loop__1__i) .
+H2: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H4: loop__1__i >= 0 .
+H5: loop__1__i <= 9 .
+H6: integer__size >= 0 .
+H7: complex_types__day__size >= 0 .
+H8: complex_types__array_index__size >= 0 .
+H9: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized2(fld_field1(element(a, [loop__1__i])), 0) .
+
+
+For path(s) from assertion of line 15 to assertion of line 10:
+
+procedure_initialize_4.
+H1: complex_types__initialized(a, loop__1__i) .
+H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])),
+ loop__2__j) .
+H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])),
+ loop__2__j, complex_types__day__pos(complex_types__sun)) .
+H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H6: loop__2__j >= 0 .
+H7: loop__1__i >= 0 .
+H8: loop__1__i <= 9 .
+H9: loop__2__j < 9 .
+H10: integer__size >= 0 .
+H11: complex_types__day__size >= 0 .
+H12: complex_types__array_index__size >= 0 .
+H13: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a,
+ [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [
+ loop__2__j, complex_types__sun], 0))), loop__1__i) .
+C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])),
+ [loop__2__j, complex_types__sun], 0), loop__2__j + 1) .
+C3: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [
+ loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [
+ i___2, i___3]) and element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [
+ loop__1__i])), [loop__2__j, complex_types__sun], 0))), [i___1])), [
+ i___2, i___3]) <= 2147483647))) .
+
+
+For path(s) from assertion of line 10 to assertion of line 15:
+
+procedure_initialize_5.
+H1: complex_types__initialized(a, loop__1__i) .
+H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])),
+ loop__2__j) .
+H3: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H5: loop__2__j >= 0 .
+H6: loop__2__j <= 9 .
+H7: loop__1__i >= 0 .
+H8: loop__1__i <= 9 .
+H9: integer__size >= 0 .
+H10: complex_types__day__size >= 0 .
+H11: complex_types__array_index__size >= 0 .
+H12: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized3(fld_field1(element(a, [loop__1__i])),
+ loop__2__j, 0) .
+
+
+For path(s) from assertion of line 15 to assertion of line 15:
+
+procedure_initialize_6.
+H1: complex_types__initialized(a, loop__1__i) .
+H2: complex_types__initialized2(fld_field1(element(a, [loop__1__i])),
+ loop__2__j) .
+H3: complex_types__initialized3(fld_field1(element(a, [loop__1__i])),
+ loop__2__j, complex_types__day__pos(loop__3__k)) .
+H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H6: complex_types__mon <= loop__3__k .
+H7: loop__2__j >= 0 .
+H8: loop__2__j <= 9 .
+H9: loop__1__i >= 0 .
+H10: loop__1__i <= 9 .
+H11: loop__3__k < complex_types__sun .
+H12: integer__size >= 0 .
+H13: complex_types__day__size >= 0 .
+H14: complex_types__array_index__size >= 0 .
+H15: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized(update(a, [loop__1__i], upf_field1(element(a,
+ [loop__1__i]), update(fld_field1(element(a, [loop__1__i])), [
+ loop__2__j, loop__3__k], 0))), loop__1__i) .
+C2: complex_types__initialized2(update(fld_field1(element(a, [loop__1__i])),
+ [loop__2__j, loop__3__k], 0), loop__2__j) .
+C3: complex_types__initialized3(update(fld_field1(element(a, [loop__1__i])),
+ [loop__2__j, loop__3__k], 0), loop__2__j, complex_types__day__pos(
+ succ(loop__3__k))) .
+C4: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [
+ loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(update(a, [loop__1__i],
+ upf_field1(element(a, [loop__1__i]), update(fld_field1(element(a, [
+ loop__1__i])), [loop__2__j, loop__3__k], 0))), [i___1])), [i___2,
+ i___3]) <= 2147483647))) .
+
+
+For path(s) from assertion of line 15 to run-time check associated with
+ statement of line 22:
+
+procedure_initialize_7.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 15 to run-time check associated with
+ statement of line 25:
+
+procedure_initialize_8.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 15 to finish:
+
+procedure_initialize_9.
+H1: complex_types__initialized(a, 9) .
+H2: complex_types__initialized2(fld_field1(element(a, [9])), 9) .
+H3: complex_types__initialized3(fld_field1(element(a, [9])), 9,
+ complex_types__day__pos(complex_types__sun)) .
+H4: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9 -> - 2147483648 <=
+ fld_field2(element(a, [i___1])) and fld_field2(element(a, [i___1]))
+ <= 2147483647) .
+H5: for_all(i___3 : complex_types__day, complex_types__mon <= i___3 and
+ i___3 <= complex_types__sun -> for_all(i___2 : integer, 0 <= i___2
+ and i___2 <= 9 -> for_all(i___1 : integer, 0 <= i___1 and i___1 <= 9
+ -> - 2147483648 <= element(fld_field1(element(a, [i___1])), [i___2,
+ i___3]) and element(fld_field1(element(a, [i___1])), [i___2, i___3])
+ <= 2147483647))) .
+H6: integer__size >= 0 .
+H7: complex_types__day__size >= 0 .
+H8: complex_types__array_index__size >= 0 .
+H9: complex_types__record_type__size >= 0 .
+ ->
+C1: complex_types__initialized(update(a, [9], upf_field1(upf_field2(element(
+ a, [9]), 0), update(fld_field1(element(a, [9])), [9,
+ complex_types__sun], 0))), 10) .
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/Gcd.adb Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,17 @@
+package body Greatest_Common_Divisor
+is
+
+ procedure G_C_D(M, N: in Natural; G: out Natural)
+ is
+ C, D, R: Integer;
+ begin
+ C := M; D := N;
+ while D /= 0 loop
+ --# assert C >= 0 and D > 0 and Gcd(C, D) = Gcd(M, N);
+ R := C rem D;
+ C := D; D := R;
+ end loop;
+ G := C;
+ end G_C_D;
+
+end Greatest_Common_Divisor;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/Gcd.ads Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,11 @@
+package Greatest_Common_Divisor
+is
+
+ --# function Gcd(A, B: Natural) return Natural;
+
+ procedure G_C_D(M, N: in Natural; G: out Natural);
+ --# derives G from M, N;
+ --# pre M >= 0 and N > 0;
+ --# post G = Gcd(M,N);
+
+end Greatest_Common_Divisor;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/Simple_Gcd.adb Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,18 @@
+package body Simple_Greatest_Common_Divisor
+is
+
+ procedure G_C_D (M, N : in Natural; G : out Natural)
+ is
+ C, D, R : Natural;
+ begin
+ C := M; D := N;
+ while D /= 0
+ --# assert Gcd (C, D) = Gcd (M, N);
+ loop
+ R := C mod D;
+ C := D; D := R;
+ end loop;
+ G := C;
+ end G_C_D;
+
+end Simple_Greatest_Common_Divisor;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/Simple_Gcd.ads Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,11 @@
+package Simple_Greatest_Common_Divisor
+is
+
+ --# function Gcd (A, B : Natural) return Natural;
+
+ procedure G_C_D (M, N : in Natural; G : out Natural);
+ --# derives G from M, N;
+ --# pre N > 0;
+ --# post G = Gcd (M, N);
+
+end Simple_Greatest_Common_Divisor;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/complex_types.ads Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,27 @@
+package Complex_Types
+is
+
+ type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
+
+ subtype Array_Index is Natural range 0 .. 9;
+
+ type Array_Type1 is array (Array_Index, Day) of Integer;
+
+ type Record_Type is
+ record
+ Field1 : Array_Type1;
+ Field2 : Integer;
+ end record;
+
+ type Array_Type2 is array (Array_Index) of Record_Type;
+
+ --# function Initialized
+ --# (A: Array_Type2; I : Natural) return Boolean;
+
+ --# function Initialized2
+ --# (A: Array_Type1; I : Natural) return Boolean;
+
+ --# function Initialized3
+ --# (A: Array_Type1; I : Natural; K : Natural) return Boolean;
+
+end Complex_Types;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/complex_types_app.adb Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,29 @@
+package body Complex_Types_App
+is
+
+ procedure Initialize (A : in out Complex_Types.Array_Type2)
+ is
+ begin
+ for I in Complex_Types.Array_Index
+ --# assert Complex_Types.Initialized (A, I);
+ loop
+ for J in Complex_Types.Array_Index
+ --# assert
+ --# Complex_Types.Initialized (A, I) and
+ --# Complex_Types.Initialized2 (A (I).Field1, J);
+ loop
+ for K in Complex_Types.Day
+ --# assert
+ --# Complex_Types.Initialized (A, I) and
+ --# Complex_Types.Initialized2 (A (I).Field1, J) and
+ --# Complex_Types.Initialized3
+ --# (A (I).Field1, J, Complex_Types.Day'Pos (K));
+ loop
+ A (I).Field1 (J, K) := 0;
+ end loop;
+ end loop;
+ A (I).Field2 := 0;
+ end loop;
+ end Initialize;
+
+end Complex_Types_App;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/complex_types_app.ads Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,11 @@
+with Complex_Types;
+--# inherit Complex_Types;
+
+package Complex_Types_App
+is
+
+ procedure Initialize (A : in out Complex_Types.Array_Type2);
+ --# derives A from A;
+ --# post Complex_Types.Initialized (A, 10);
+
+end Complex_Types_App;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/intro.tex Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,129 @@
+\chapter{Introduction}
+\label{sec:intro}
+
+This document describes a link between Isabelle/HOL and the \SPARK{}/Ada tool
+suite for the verification of high-integrity software.
+Using this link, verification problems can be tackled that are beyond reach
+of the proof tools currently available for \SPARK{}. A number of examples
+can be found in the directory \texttt{HOL/SPARK/Examples} in the Isabelle
+distribution. An open-source version of the \SPARK{} tool suite is available
+free of charge from \hbox{\href{http://libre.adacore.com}{libre.adacore.com}}.
+
+In the remainder of \secref{sec:intro},
+we give an introduction to \SPARK{} and the HOL-\SPARK{} link. The verification
+of an example program is described in \secref{sec:example-verification}. In
+\secref{sec:vc-principles}, we explain the principles underlying the generation
+of verification conditions for \SPARK{} programs. Finally, \secref{sec:spark-reference}
+describes the commands provided by the HOL-\SPARK{} link, as well as the encoding
+of \SPARK{} types in HOL.
+
+\section{\SPARK{}}
+
+\SPARK{} \cite{Barnes} is a subset of the Ada language that has been designed to
+allow verification of high-integrity software. It is missing certain features of
+Ada that can make programs difficult to verify, such as \emph{access types},
+\emph{dynamic data structures}, and \emph{recursion}. \SPARK{} allows to prove
+absence of \emph{runtime exceptions}, as well as \emph{partial correctness}
+using pre- and postconditions. Loops can be annotated with \emph{invariants},
+and each procedure must have a \emph{dataflow annotation}, specifying the
+dependencies of the output parameters on the input parameters of the procedure.
+Since \SPARK{} annotations are just written as comments, \SPARK{} programs can be
+compiled by an ordinary Ada compiler such as GNAT. \SPARK{} comes with a number
+of tools, notably the \emph{Examiner} that, given a \SPARK{} program as an input,
+performs a \emph{dataflow analysis} and generates \emph{verification conditions}
+(VCs) that must be proved in order for the program to be exception-free and partially
+correct. The VCs generated by the Examiner are formulae expressed in
+a language called FDL, which is first-order logic extended with
+arithmetic operators, arrays, records, and enumeration types. For example,
+the FDL expression
+\begin{alltt}
+ for_all(i: integer, ((i >= min) and (i <= max)) ->
+ (element(a, [i]) = 0))
+\end{alltt}
+states that all elements of the array \texttt{a} with indices greater or equal to
+\texttt{min} and smaller or equal to \texttt{max} are $0$.
+VCs are processed by another \SPARK{} tool called the
+\emph{Simplifier} that either completely solves VCs or transforms them
+into simpler, equivalent conditions. The latter VCs
+can then be processed using another tool called
+the \emph{Proof Checker}. While the Simplifier tries to prove VCs in a completely
+automatic way, the Proof Checker requires user interaction, which enables it to
+prove formulae that are beyond the scope of the Simplifier. The steps
+that are required to manually prove a VC are recorded in a log file by the Proof
+Checker. Finally, this log file, together with the output of the other \SPARK{} tools
+mentioned above, is read by a tool called POGS (\textbf{P}roof \textbf{O}bli\textbf{G}ation
+\textbf{S}ummariser) that produces a table mentioning for each VC the method by which
+it has been proved.
+In order to overcome the limitations of FDL and to express complex specifications,
+\SPARK{} allows the user to declare so-called
+\emph{proof functions}. The desired properties of such functions are described
+by postulating a set of rules that can be used by the Simplifier and Proof Checker
+\cite[\S 11.7]{Barnes}. An obvious drawback of this approach is that incorrect
+rules can easily introduce inconsistencies.
+
+\section{HOL-\SPARK{}}
+
+The HOL-\SPARK{} verification environment, which is built on top of Isabelle's object
+logic HOL, is intended as an alternative
+to the \SPARK{} Proof Checker, and improves on it in a number of ways.
+HOL-\SPARK{} allows Isabelle to directly parse files generated
+by the Examiner and Simplifier, and provides a special proof command to conduct
+proofs of VCs, which can make use of the full power of Isabelle's rich
+collection of proof methods.
+Proofs can be conducted using Isabelle's graphical user interface, which makes
+it easy to navigate through larger proof scripts. Moreover, proof functions
+can be introduced in a \emph{definitional} way, for example by using Isabelle's
+package for recursive functions, rather than by just stating their properties as axioms,
+which avoids introducing inconsistencies.
+
+\begin{figure}
+\begin{center}
+\begin{tikzpicture}
+\tikzstyle{box}=[draw, drop shadow, fill=white, text width=3.5cm, text centered]
+\tikzstyle{rbox}=[draw, drop shadow, fill=white, rounded corners, minimum height=1cm]
+
+\node[box] (src) at (5,0) {Source files (\texttt{*.ads, *.adb})};
+\node[rbox] (exa) at (5,-2) {Examiner};
+\node[box] (fdl) at (0.5,-4) {FDL declarations \\ (\texttt{*.fdl})};
+\node[box] (vcs) at (5,-4) {VCs \\ (\texttt{*.vcg})};
+\node[box] (rls) at (9.5,-4) {Rules \\ (\texttt{*.rls})};
+\node[rbox] (simp) at (5,-6) {Simplifier};
+\node[box] (siv) at (5,-8) {Simplified VCs \\ (\texttt{*.siv})};
+\node[rbox] (isa) at (5,-10) {HOL-\SPARK{}};
+\node[box] (thy) at (9.5,-10) {Theory files \\ (\texttt{*.thy})};
+\node[box] (prv) at (5,-12) {Proof review files \\ (\texttt{*.prv})};
+\node[rbox] (pogs) at (5,-14) {POGS};
+\node[box] (sum) at (5,-16) {Summary file \\ (\texttt{*.sum})};
+
+\draw[-latex] (src) -- (exa);
+\draw[-latex] (exa) -- (fdl);
+\draw[-latex] (exa) -- (vcs);
+\draw[-latex] (exa) -- (rls);
+\draw[-latex] (fdl) -- (simp);
+\draw[-latex] (vcs) -- (simp);
+\draw[-latex] (rls) -- (simp);
+\draw[-latex] (simp) -- (siv);
+\draw[-latex] (fdl) .. controls (0.5,-8) .. (isa);
+\draw[-latex] (siv) -- (isa);
+\draw[-latex] (rls) .. controls (9.5,-8) .. (isa);
+\draw[-latex] (thy) -- (isa);
+\draw[-latex] (isa) -- (prv);
+\draw[-latex] (vcs) .. controls (-1,-6) and (-1,-13) .. (pogs);
+\draw[-latex] (siv) .. controls (1,-9) and (1,-12) .. (pogs);
+\draw[-latex] (prv) -- (pogs);
+\draw[-latex] (pogs) -- (sum);
+\end{tikzpicture}
+\end{center}
+\caption{\SPARK{} program verification tool chain}
+\label{fig:spark-toolchain}
+\end{figure}
+Figure \ref{fig:spark-toolchain} shows the integration of HOL-\SPARK{} into the
+tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
+(\texttt{*.fdl}) and rules (\texttt{*.rls}) produced by the Examiner, as well as
+simplified VCs (\texttt{*.siv}) produced by the \SPARK{} Simplifier. Alternatively,
+the original unsimplified VCs (\texttt{*.vcg}) produced by the Examiner can be
+used as well. Processing of the \SPARK{} files is triggered by an Isabelle
+theory file (\texttt{*.thy}), which also contains the proofs for the VCs contained
+in the \texttt{*.siv} or \texttt{*.vcg} files. Once that all verification conditions
+have been successfully proved, Isabelle generates a proof review file (\texttt{*.prv})
+notifying the POGS tool of the VCs that have been discharged.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/loop_invariant.adb Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,27 @@
+package body Loop_Invariant
+is
+
+ procedure Proc1 (A : in Natural; B : in Word32; C : out Word32)
+ is
+ begin
+ C := 0;
+ for I in Natural range 1 .. A
+ --# assert Word32 (I - 1) * B = C;
+ loop
+ C := C + B;
+ end loop;
+ end Proc1;
+
+ procedure Proc2 (A : in Natural; B : in Word32; C : out Word32)
+ is
+ begin
+ C := 0;
+ for I in Natural range 1 .. A
+ --# assert Word32 (I - 1) * B = C;
+ loop
+ C := C + B;
+ --# assert Word32 (I) * B = C;
+ end loop;
+ end Proc2;
+
+end Loop_Invariant;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/loop_invariant.ads Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,14 @@
+package Loop_Invariant
+is
+
+ type Word32 is mod 2 ** 32;
+
+ procedure Proc1 (A : in Natural; B : in Word32; C : out Word32);
+ --# derives C from A, B;
+ --# post Word32 (A) * B = C;
+
+ procedure Proc2 (A : in Natural; B : in Word32; C : out Word32);
+ --# derives C from A, B;
+ --# post Word32 (A) * B = C;
+
+end Loop_Invariant;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/root.bib Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,7 @@
+@Book{Barnes,
+ author = {John Barnes},
+ title = {{T}he \textsc{Spark} {A}pproach to {S}afety and
+ {S}ecurity},
+ publisher = {Addison-Wesley},
+ year = 2006
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/root.tex Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,83 @@
+\documentclass[12pt,a4paper]{report}
+
+\usepackage[a4paper,hscale=0.65,vscale=0.71,hcentering,vcentering]{geometry}
+
+\usepackage{isabelle,isabellesym}
+
+\usepackage{charter}
+
+\usepackage{tikz}
+\usetikzlibrary{shadows}
+
+\usepackage{listings}
+
+\usepackage{alltt}
+
+\usepackage{railsetup}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{tt}
+
+\renewcommand{\isastyleminor}{\tt}
+
+\lstdefinelanguage{SPARK}[95]{Ada} {
+ morecomment=*[l]{--\#},
+ morekeywords=
+ {
+ inherit, own, initializes, hide, global, main_program,
+ derives, from, pre, post, return, assert, check
+ }
+}
+
+\lstset{ %
+language=SPARK,
+basicstyle=\small\ttfamily,
+keywordstyle=\rmfamily\bfseries,
+columns=flexible,
+showstringspaces=false
+}
+
+\newcommand{\mod}{\mathbin{\hbox{\textbf{mod}}}}
+
+\newcommand{\SPARK}{\textsc{Spark}}
+
+\newcommand{\secref}[1]{\S \ref{#1}}
+\newcommand{\figref}[1]{Fig.\ \ref{#1}}
+
+\renewcommand{\topfraction}{.99}
+\renewcommand{\bottomfraction}{.99}
+\setcounter{topnumber}{9}
+\setcounter{bottomnumber}{9}
+\setcounter{totalnumber}{20}
+
+
+\begin{document}
+
+\title{The HOL-\SPARK{} Program Verification Environment}
+\author{\emph{Stefan Berghofer} \\ \emph{secunet Security Networks AG}}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+\input{intro}
+\input{Example_Verification}
+\input{VC_Principles}
+\input{Reference}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc1.fdl Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,38 @@
+ {*******************************************************}
+ {FDL Declarations}
+ {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039}
+ {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.}
+ {*******************************************************}
+
+
+ {DATE : 22-SEP-2011 11:10:50.40}
+
+ {procedure Loop_Invariant.Proc1}
+
+
+title procedure proc1;
+
+ function round__(real) : integer;
+ type word32 = integer;
+ const word32__base__first : integer = pending;
+ const word32__base__last : integer = pending;
+ const natural__base__first : integer = pending;
+ const natural__base__last : integer = pending;
+ const integer__base__first : integer = pending;
+ const integer__base__last : integer = pending;
+ const word32__first : integer = pending;
+ const word32__last : integer = pending;
+ const word32__modulus : integer = pending;
+ const word32__size : integer = pending;
+ const natural__first : integer = pending;
+ const natural__last : integer = pending;
+ const natural__size : integer = pending;
+ const integer__first : integer = pending;
+ const integer__last : integer = pending;
+ const integer__size : integer = pending;
+ var a : integer;
+ var b : integer;
+ var c : integer;
+ var loop__1__i : integer;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc1.rls Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,33 @@
+ /*********************************************************/
+ /*Proof Rule Declarations*/
+ /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
+ /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
+ /*********************************************************/
+
+
+ /*DATE : 22-SEP-2011 11:10:50.40*/
+
+ /*procedure Loop_Invariant.Proc1*/
+
+
+rule_family proc1_rules:
+ X requires [X:any] &
+ X <= Y requires [X:ire, Y:ire] &
+ X >= Y requires [X:ire, Y:ire].
+
+proc1_rules(1): integer__size >= 0 may_be_deduced.
+proc1_rules(2): integer__first may_be_replaced_by -2147483648.
+proc1_rules(3): integer__last may_be_replaced_by 2147483647.
+proc1_rules(4): integer__base__first may_be_replaced_by -2147483648.
+proc1_rules(5): integer__base__last may_be_replaced_by 2147483647.
+proc1_rules(6): natural__size >= 0 may_be_deduced.
+proc1_rules(7): natural__first may_be_replaced_by 0.
+proc1_rules(8): natural__last may_be_replaced_by 2147483647.
+proc1_rules(9): natural__base__first may_be_replaced_by -2147483648.
+proc1_rules(10): natural__base__last may_be_replaced_by 2147483647.
+proc1_rules(11): word32__size >= 0 may_be_deduced.
+proc1_rules(12): word32__first may_be_replaced_by 0.
+proc1_rules(13): word32__last may_be_replaced_by 4294967295.
+proc1_rules(14): word32__base__first may_be_replaced_by 0.
+proc1_rules(15): word32__base__last may_be_replaced_by 4294967295.
+proc1_rules(16): word32__modulus may_be_replaced_by 4294967296.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc1.siv Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,93 @@
+*****************************************************************************
+ Semantic Analysis of SPARK Text
+ Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+ Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+*****************************************************************************
+
+
+CREATED 22-SEP-2011, 11:10:50 SIMPLIFIED 22-SEP-2011, 11:10:51
+
+SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+
+procedure Loop_Invariant.Proc1
+
+
+
+
+For path(s) from start to run-time check associated with statement of line 7:
+
+procedure_proc1_1.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to run-time check associated with statement of line 8:
+
+procedure_proc1_2.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to run-time check associated with statement of line 8:
+
+procedure_proc1_3.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to assertion of line 8:
+
+procedure_proc1_4.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 8 to assertion of line 8:
+
+procedure_proc1_5.
+H1: a <= 2147483647 .
+H2: b >= 0 .
+H3: b <= 4294967295 .
+H4: loop__1__i >= 1 .
+H5: (loop__1__i - 1) * b mod 4294967296 >= 0 .
+H6: (loop__1__i - 1) * b mod 4294967296 <= 4294967295 .
+H7: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
+H8: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
+H9: loop__1__i < a .
+H10: integer__size >= 0 .
+H11: natural__size >= 0 .
+H12: word32__size >= 0 .
+ ->
+C1: loop__1__i * b mod 4294967296 = ((loop__1__i - 1) * b mod 4294967296 + b)
+ mod 4294967296 .
+
+
+For path(s) from assertion of line 8 to run-time check associated with
+ statement of line 11:
+
+procedure_proc1_6.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to finish:
+
+procedure_proc1_7.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 8 to finish:
+
+procedure_proc1_8.
+H1: a <= 2147483647 .
+H2: b >= 0 .
+H3: b <= 4294967295 .
+H4: a <= 2147483647 .
+H5: a >= 1 .
+H6: (a - 1) * b mod 4294967296 >= 0 .
+H7: (a - 1) * b mod 4294967296 <= 4294967295 .
+H8: ((a - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
+H9: ((a - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
+H10: integer__size >= 0 .
+H11: natural__size >= 0 .
+H12: word32__size >= 0 .
+ ->
+C1: a * b mod 4294967296 = ((a - 1) * b mod 4294967296 + b) mod 4294967296 .
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc2.fdl Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,38 @@
+ {*******************************************************}
+ {FDL Declarations}
+ {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039}
+ {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.}
+ {*******************************************************}
+
+
+ {DATE : 22-SEP-2011 11:10:50.42}
+
+ {procedure Loop_Invariant.Proc2}
+
+
+title procedure proc2;
+
+ function round__(real) : integer;
+ type word32 = integer;
+ const word32__base__first : integer = pending;
+ const word32__base__last : integer = pending;
+ const natural__base__first : integer = pending;
+ const natural__base__last : integer = pending;
+ const integer__base__first : integer = pending;
+ const integer__base__last : integer = pending;
+ const word32__first : integer = pending;
+ const word32__last : integer = pending;
+ const word32__modulus : integer = pending;
+ const word32__size : integer = pending;
+ const natural__first : integer = pending;
+ const natural__last : integer = pending;
+ const natural__size : integer = pending;
+ const integer__first : integer = pending;
+ const integer__last : integer = pending;
+ const integer__size : integer = pending;
+ var a : integer;
+ var b : integer;
+ var c : integer;
+ var loop__1__i : integer;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc2.rls Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,33 @@
+ /*********************************************************/
+ /*Proof Rule Declarations*/
+ /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
+ /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
+ /*********************************************************/
+
+
+ /*DATE : 22-SEP-2011 11:10:50.42*/
+
+ /*procedure Loop_Invariant.Proc2*/
+
+
+rule_family proc2_rules:
+ X requires [X:any] &
+ X <= Y requires [X:ire, Y:ire] &
+ X >= Y requires [X:ire, Y:ire].
+
+proc2_rules(1): integer__size >= 0 may_be_deduced.
+proc2_rules(2): integer__first may_be_replaced_by -2147483648.
+proc2_rules(3): integer__last may_be_replaced_by 2147483647.
+proc2_rules(4): integer__base__first may_be_replaced_by -2147483648.
+proc2_rules(5): integer__base__last may_be_replaced_by 2147483647.
+proc2_rules(6): natural__size >= 0 may_be_deduced.
+proc2_rules(7): natural__first may_be_replaced_by 0.
+proc2_rules(8): natural__last may_be_replaced_by 2147483647.
+proc2_rules(9): natural__base__first may_be_replaced_by -2147483648.
+proc2_rules(10): natural__base__last may_be_replaced_by 2147483647.
+proc2_rules(11): word32__size >= 0 may_be_deduced.
+proc2_rules(12): word32__first may_be_replaced_by 0.
+proc2_rules(13): word32__last may_be_replaced_by 4294967295.
+proc2_rules(14): word32__base__first may_be_replaced_by 0.
+proc2_rules(15): word32__base__last may_be_replaced_by 4294967295.
+proc2_rules(16): word32__modulus may_be_replaced_by 4294967296.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/loop_invariant/proc2.siv Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,87 @@
+*****************************************************************************
+ Semantic Analysis of SPARK Text
+ Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+ Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+*****************************************************************************
+
+
+CREATED 22-SEP-2011, 11:10:50 SIMPLIFIED 22-SEP-2011, 11:10:51
+
+SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+
+procedure Loop_Invariant.Proc2
+
+
+
+
+For path(s) from start to run-time check associated with statement of line 18:
+
+procedure_proc2_1.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to run-time check associated with statement of line 19:
+
+procedure_proc2_2.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to run-time check associated with statement of line 19:
+
+procedure_proc2_3.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to assertion of line 19:
+
+procedure_proc2_4.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 23 to assertion of line 19:
+
+procedure_proc2_5.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 19 to run-time check associated with
+ statement of line 22:
+
+procedure_proc2_6.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 19 to assertion of line 23:
+
+procedure_proc2_7.
+H1: a <= 2147483647 .
+H2: b >= 0 .
+H3: b <= 4294967295 .
+H4: loop__1__i <= 2147483647 .
+H5: loop__1__i >= 1 .
+H6: loop__1__i <= a .
+H7: (loop__1__i - 1) * b mod 4294967296 >= 0 .
+H8: (loop__1__i - 1) * b mod 4294967296 <= 4294967295 .
+H9: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 >= 0 .
+H10: ((loop__1__i - 1) * b mod 4294967296 + b) mod 4294967296 <= 4294967295 .
+H11: integer__size >= 0 .
+H12: natural__size >= 0 .
+H13: word32__size >= 0 .
+ ->
+C1: loop__1__i * b mod 4294967296 = ((loop__1__i - 1) * b mod 4294967296 + b)
+ mod 4294967296 .
+
+
+For path(s) from start to finish:
+
+procedure_proc2_8.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 23 to finish:
+
+procedure_proc2_9.
+*** true . /* all conclusions proved */
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,32 @@
+ {*******************************************************}
+ {FDL Declarations}
+ {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039}
+ {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.}
+ {*******************************************************}
+
+
+ {DATE : 22-SEP-2011 11:10:48.96}
+
+ {procedure Simple_Greatest_Common_Divisor.G_C_D}
+
+
+title procedure g_c_d;
+
+ function round__(real) : integer;
+ const natural__base__first : integer = pending;
+ const natural__base__last : integer = pending;
+ const integer__base__first : integer = pending;
+ const integer__base__last : integer = pending;
+ const natural__first : integer = pending;
+ const natural__last : integer = pending;
+ const natural__size : integer = pending;
+ const integer__first : integer = pending;
+ const integer__last : integer = pending;
+ const integer__size : integer = pending;
+ var m : integer;
+ var n : integer;
+ var c : integer;
+ var d : integer;
+ function gcd(integer, integer) : integer;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,27 @@
+ /*********************************************************/
+ /*Proof Rule Declarations*/
+ /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
+ /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
+ /*********************************************************/
+
+
+ /*DATE : 22-SEP-2011 11:10:48.96*/
+
+ /*procedure Simple_Greatest_Common_Divisor.G_C_D*/
+
+
+rule_family g_c_d_rules:
+ X requires [X:any] &
+ X <= Y requires [X:ire, Y:ire] &
+ X >= Y requires [X:ire, Y:ire].
+
+g_c_d_rules(1): integer__size >= 0 may_be_deduced.
+g_c_d_rules(2): integer__first may_be_replaced_by -2147483648.
+g_c_d_rules(3): integer__last may_be_replaced_by 2147483647.
+g_c_d_rules(4): integer__base__first may_be_replaced_by -2147483648.
+g_c_d_rules(5): integer__base__last may_be_replaced_by 2147483647.
+g_c_d_rules(6): natural__size >= 0 may_be_deduced.
+g_c_d_rules(7): natural__first may_be_replaced_by 0.
+g_c_d_rules(8): natural__last may_be_replaced_by 2147483647.
+g_c_d_rules(9): natural__base__first may_be_replaced_by -2147483648.
+g_c_d_rules(10): natural__base__last may_be_replaced_by 2147483647.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv Thu Sep 22 16:56:19 2011 +0200
@@ -0,0 +1,99 @@
+*****************************************************************************
+ Semantic Analysis of SPARK Text
+ Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+ Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+*****************************************************************************
+
+
+CREATED 22-SEP-2011, 11:10:48 SIMPLIFIED 22-SEP-2011, 11:10:49
+
+SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+
+procedure Simple_Greatest_Common_Divisor.G_C_D
+
+
+
+
+For path(s) from start to run-time check associated with statement of line 8:
+
+procedure_g_c_d_1.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to run-time check associated with statement of line 8:
+
+procedure_g_c_d_2.
+*** true . /* all conclusions proved */
+
+
+For path(s) from start to assertion of line 9:
+
+procedure_g_c_d_3.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 9 to assertion of line 9:
+
+procedure_g_c_d_4.
+H1: gcd(c, d) = gcd(m, n) .
+H2: m >= 0 .
+H3: m <= 2147483647 .
+H4: n <= 2147483647 .
+H5: n > 0 .
+H6: d <= 2147483647 .
+H7: c >= 0 .
+H8: c <= 2147483647 .
+H9: c mod d >= 0 .
+H10: c mod d <= 2147483647 .
+H11: 0 < d .
+H12: integer__size >= 0 .
+H13: natural__size >= 0 .
+ ->
+C1: gcd(d, c mod d) = gcd(m, n) .
+
+
+For path(s) from assertion of line 9 to run-time check associated with
+ statement of line 12:
+
+procedure_g_c_d_5.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 9 to run-time check associated with
+ statement of line 13:
+
+procedure_g_c_d_6.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 9 to run-time check associated with
+ statement of line 13:
+
+procedure_g_c_d_7.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 9 to run-time check associated with
+ statement of line 15:
+
+procedure_g_c_d_8.
+*** true . /* all conclusions proved */
+
+
+For path(s) from assertion of line 9 to finish:
+
+procedure_g_c_d_9.
+H1: gcd(c, 0) = gcd(m, n) .
+H2: m >= 0 .
+H3: m <= 2147483647 .
+H4: n <= 2147483647 .
+H5: n > 0 .
+H6: c >= 0 .
+H7: c <= 2147483647 .
+H8: integer__size >= 0 .
+H9: natural__size >= 0 .
+ ->
+C1: c = gcd(m, n) .
+
+