Quelle Reference.thy

Sprache: Isabelle

(*<*)
theory Reference
imports "HOL-SPARK.SPARK"
begin

unbundle bit_operations_syntax

lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int
by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod)

syntax (my_constrain output)
"_constrain" :: "logic => type => logic" (‹_ :: _› [4, 0] 3)
(*>*)

chapter ‹HOL-\SPARK{} Reference›

text ‹
label{sec:spark-reference}
section is intended as a quick reference for the HOL-\SPARK{} verification
. In \secref{sec:spark-commands}, we give a summary of the commands
by the HOL-\SPARK{}, while \secref{sec:spark-types} contains a description
how particular types of \SPARK{} and FDL are modelled in Isabelle.
›

section ‹Commands›

text ‹
label{sec:spark-commands}
section describes the syntax and effect of each of the commands provided
HOL-\SPARK{}.
🚫‹
@'spark_open' name ('(' name ')')?
›
a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
corresponding \texttt{*.fdl} and \texttt{*.rls}
must reside in the same directory as the file given as an argument to the command.
command also generates records and datatypes for the types specified in the
texttt{*.fdl} file, unless they have already been associated with user-defined
types (see below).
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
\texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
, this is necessary in order for the verification environment to be able to map proof
and types defined in Isabelle to their \SPARK{} counterparts.
🚫‹
@'spark_proof_functions' ((name '=' term)+)
›
a proof function with the given name to a term. The name should be the full name
the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
command can be used both inside and outside a verification environment. The latter
is useful for introducing proof functions that are shared by several procedures
packages, whereas the former allows the given term to refer to the types generated
\isa{\isacommand{spark\_open}} for record or enumeration types specified in the
texttt{*.fdl} file.
🚫‹
@'spark_types' ((name '=' type (mapping?))+)
;
mapping: '('((name '=' name)+',')')'
›
a \SPARK{} type with the given name with an Isabelle type. This command can
be used outside a verification environment. The given type must be either a record
a datatype, where the names of fields or constructors must either match those of the
\SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle
has to be provided.
command is useful when having to define
functions referring to record or enumeration types that are shared by several
or packages. First, the types required by the proof functions can be introduced
Isabelle's commands for defining records or datatypes. Having introduced the
, the proof functions can be defined in Isabelle. Finally, both the proof
and the types can be associated with their \SPARK{} counterparts.
🚫‹
@'spark_status' (('(proved)' | '(unproved)')?)
›
the variables declared in the \texttt{*.fdl} file, the rules declared in
\texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
output can be restricted to the proved or unproved VCs by giving the corresponding
to the command.
🚫‹
@'spark_vc' name
›
the proof of the VC with the given name. Similar to the standard
isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
be followed by a sequence of proof commands. The command introduces the
\texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
🚫‹
@'spark_end' '(incomplete)'?
›
the current verification environment. Unless the \texttt{incomplete}
is given, all VCs must have been proved,
the command issues an error message. As a side effect, the command
a proof review (\texttt{*.prv}) file to inform POGS of the proved
.
›

section ‹Types›

text ‹
label{sec:spark-types}
main types of FDL are integers, enumeration types, records, and arrays.
the following sections, we describe how these types are modelled in
.
›

subsection ‹Integers›

text ‹
FDL type \texttt{integer} is modelled by the Isabelle type typ‹int›.
the FDL \texttt{mod} operator behaves in the same way as its Isabelle
, this is not the case for the \texttt{div} operator. As has already
mentioned in \secref{sec:proving-vcs}, the \texttt{div} operator of \SPARK{}
truncates towards zero, whereas the ‹div› operator of Isabelle
towards minus infinity. Therefore, the FDL \texttt{div} operator is
to the ‹sdiv› operator in Isabelle. The characteristic theorems
‹sdiv›, in particular those describing the relationship with the standard
‹div› operator, are shown in \figref{fig:sdiv-properties}
begin{figure}
begin{center}
small
begin{tabular}{ll}
‹sdiv_def›: & @{thm sdiv_def} \\
‹sdiv_minus_dividend›: & @{thm sdiv_minus_dividend} \\
‹sdiv_minus_divisor›: & @{thm sdiv_minus_divisor} \\
‹sdiv_pos_pos›: & @{thm [mode=no_brackets] sdiv_pos_pos} \\
‹sdiv_pos_neg›: & @{thm [mode=no_brackets] sdiv_pos_neg} \\
‹sdiv_neg_pos›: & @{thm [mode=no_brackets] sdiv_neg_pos} \\
‹sdiv_neg_neg›: & @{thm [mode=no_brackets] sdiv_neg_neg} \\
end{tabular}
end{center}
caption{Characteristic properties of ‹sdiv›}
label{fig:sdiv-properties}
end{figure}

begin{figure}
begin{center}
small
begin{tabular}{ll}
‹AND_lower›: & @{thm [mode=no_brackets] AND_lower} \\
‹OR_lower›: & @{thm [mode=no_brackets] OR_lower} \\
‹XOR_lower›: & @{thm [mode=no_brackets] XOR_lower} \\
‹AND_upper1›: & @{thm [mode=no_brackets] AND_upper1} \\
‹AND_upper2›: & @{thm [mode=no_brackets] AND_upper2} \\
‹OR_upper›: & @{thm [mode=no_brackets] OR_upper} \\
‹XOR_upper›: & @{thm [mode=no_brackets] XOR_upper} \\
‹AND_mod›: & @{thm [mode=no_brackets] AND_mod}
end{tabular}
end{center}
caption{Characteristic properties of bitwise operators}
label{fig:bitwise}
end{figure}
bitwise logical operators of \SPARK{} and FDL are modelled by the operators
‹AND›, ‹OR› and ‹XOR› from Isabelle's ‹Word› library,
of which have type typ‹int → int → int›. A list of properties of these
that are useful in proofs about \SPARK{} programs are shown in
figref{fig:bitwise}
›

subsection ‹Enumeration types›

text ‹
FDL enumeration type
begin{alltt}
$t$ = ($e\sb{1}$, $e\sb{2}$, \dots, $e\sb{n}$);
end{alltt}
modelled by the Isabelle datatype
begin{isabelle}
normalsize
isacommand{datatype}\ $t$\ =\ $e_1$\ $\mid$\ $e_2$\ $\mid$\ \dots\ $\mid$\ $e_n$
end{isabelle}
HOL-\SPARK{} environment defines a type class 🚫‹spark_enum› that captures
characteristic properties of all enumeration types. It provides the following
functions and constants for all types ‹'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}
addition, 🚫‹spark_enum› is a subclass of the 🚫‹linorder› type class,
allows the comparison operators ‹<\<close> and ‹≤› to be used on
types. The polymorphic operations shown above enjoy a number of
properties that hold for all enumeration types. These properties are
in \figref{fig:enum-generic-properties}.
, \figref{fig:enum-specific-properties} shows a list of properties
are specific to each enumeration type $t$, such as the characteristic
for term‹val› and term‹pos›.
begin{figure}[t]
begin{center}
small
begin{tabular}{ll}
‹range_pos›: & @{thm range_pos} \\
‹less_pos›: & @{thm less_pos} \\
‹less_eq_pos›: & @{thm less_eq_pos} \\
‹val_def›: & @{thm val_def} \\
‹succ_def›: & @{thm succ_def} \\
‹pred_def›: & @{thm pred_def} \\
‹first_el_def›: & @{thm first_el_def} \\
‹last_el_def›: & @{thm last_el_def} \\
‹inj_pos›: & @{thm inj_pos} \\
‹val_pos›: & @{thm val_pos} \\
‹pos_val›: & @{thm pos_val} \\
‹first_el_smallest›: & @{thm first_el_smallest} \\
‹last_el_greatest›: & @{thm last_el_greatest} \\
‹pos_succ›: & @{thm pos_succ} \\
‹pos_pred›: & @{thm pos_pred} \\
‹succ_val›: & @{thm succ_val} \\
‹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$} & 'color:turquoise'>\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}
›

‹Records›

‹
FDL record type
begin{alltt}
$t$ = record
$f\sb{1}$ : $t\sb{1}$;
$\vdots$
$f\sb{n}$ : $t\sb{n}$
end;
end{alltt}
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}
are constructed using the notation
isa{\isasymlparr$f_1$\ =\ $v_1$,\ $\ldots$,\ $f_n$\ =\ $v_n$\isasymrparr},
field $f_i$ of a record $r$ is selected using the notation $f_i~r$, and the
$f$ and $f'$ of a record $r$ can be updated using the notation
mbox{\isa{$r$\ \isasymlparr$f$\ :=\ $v$,\ $f'$\ :=\ $v'$\isasymrparr}}.
›

‹Arrays›

‹
FDL array type
begin{alltt}
$t$ = array [$t\sb{1}$, $\ldots$, $t\sb{n}$] of $u$;
end{alltt}
modelled by the Isabelle function type $t_1 \times \cdots \times t_n \Rightarrow u$.
updates are written as \isa{$A$($x_1$\ := $y_1$,\ \dots,\ $x_n$\ :=\ $y_n$)}.
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
properties
{thm [display,mode=no_brackets] fun_upds_in fun_upds_notin upds_singleton}
, we can write expressions like
{term [display] "(A::int→int) ({0..9} [:=] 42, 15 := 99, {20..29} [:=] 0)"}
would be cumbersome to write using single updates.
›

‹User-defined proof functions and types›

‹
illustrate the interplay between the commands for introducing user-defined proof
and types mentioned in \secref{sec:spark-commands}, we now discuss a larger
involving the definition of proof functions on complex types. Assume we would
to define an array type, whose elements are records that themselves contain
. Moreover, assume we would like to initialize all array elements and record
of type \texttt{Integer} in an array of this type with the value \texttt{0}.
specification of package \texttt{Complex\_Types} containing the definition of
array type, which we call \texttt{Array\_Type2}, is shown in \figref{fig:complex-types}.
also contains the declaration of a proof function \texttt{Initialized} that is used
express that the array has been initialized. The two other proof functions
texttt{Initialized2} and \texttt{Initialized3} are used to reason about the
of the inner array. Since the array types and proof functions
be used by several packages, such as the one shown in \figref{fig:complex-types-app},
is advantageous to define the proof functions in a central theory that can
included by other theories containing proofs about packages using \texttt{Complex\_Types}.
show this theory in \figref{fig:complex-types-thy}. Since the proof functions
to the enumeration and record types defined in \texttt{Complex\_Types},
need to define the Isabelle counterparts of these types using the
isa{\isacommand{datatype}} and \isa{\isacommand{record}} commands in order
be able to write down the definition of the proof functions. These types are
to the corresponding \SPARK{} types using the \isa{\isacommand{spark\_types}}
. Note that we have to specify the full name of the \SPARK{} functions
the package prefix. Using the logic of Isabelle, we can then define
involving the enumeration and record types introduced above, and link
to the corresponding \SPARK{} proof functions. It is important that the
isa{\isacommand{definition}} commands are preceeded by the \isa{\isacommand{spark\_types}}
, since the definition of ‹initialized3› uses the ‹val›
for enumeration types that is only available once that ‹day›
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
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.