# HG changeset patch # User berghofe # Date 1316703379 -7200 # Node ID 7ac79855b1e209339846b33e66d353f65acdc4af # Parent 7e1a73fc0c8b1f19d936276ad5ccd98991607fd6# Parent 2fae15f8984df0e85a20c2108712bb14ffbfc479 merged diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/IsaMakefile --- 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 \ diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Complex_Types.thy --- /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 \ day \ int" + Field2 :: int + +spark_types + complex_types__day = day + complex_types__record_type = two_fields + +definition + initialized3 :: "(int \ day \ int) \ int \ int \ bool" where + "initialized3 A i k = (\j\{0.. day \ int) \ int \ bool" where + "initialized2 A i = (\j\{0.. two_fields) \ int \ bool" where + "initialized A i = (\j\{0.. 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 diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Example_Verification.thy --- /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 \ integer__size"}" \\ +and & @{text "g_c_d_rules6:"}\ "@{text "0 \ 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 \ 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 \ 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 \ 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 +(*>*) diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Proc1.thy --- /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 diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Proc2.thy --- /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 diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/ROOT.ML --- /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"]; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Reference.thy --- /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" ("_ \ _" [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 \ int \ 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 "\"} 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\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 +(*>*) diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy --- /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 \ int \ 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 \ c` `gcd c 0 = gcd m n` + by simp + +spark_end + +end diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/VC_Principles.thy --- /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 +(*>*) diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/complex_types_app/initialize.fdl --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/complex_types_app/initialize.rls --- /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)]. diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/complex_types_app/initialize.siv --- /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) . + + diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/Gcd.adb --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/Gcd.ads --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/Simple_Gcd.adb --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/Simple_Gcd.ads --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/complex_types.ads --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/complex_types_app.adb --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/complex_types_app.ads --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/intro.tex --- /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. diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/loop_invariant.adb --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/loop_invariant.ads --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/root.bib --- /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 +} diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/document/root.tex --- /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: diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc1.fdl --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc1.rls --- /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. diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc1.siv --- /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 . + + diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc2.fdl --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc2.rls --- /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. diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/loop_invariant/proc2.siv --- /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 */ + + diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl --- /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; diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls --- /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. diff -r 7e1a73fc0c8b -r 7ac79855b1e2 src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv --- /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) . + +