src/HOL/SPARK/Manual/Reference.thy
 changeset 59938 f84b93187ab6 parent 58130 5e9170812356 child 61143 5f898411ce87
equal inserted replaced
59937:6eccb133d4e6 59938:f84b93187ab6
    21
    21
    22 text {*
    22 text {*
    23 \label{sec:spark-commands}
    23 \label{sec:spark-commands}
    24 This section describes the syntax and effect of each of the commands provided
    24 This section describes the syntax and effect of each of the commands provided
    25 by HOL-\SPARK{}.
    25 by HOL-\SPARK{}.
    26 @{rail "@'spark_open' name ('(' name ')')?"}
    26 @{rail \<open>

    27   @'spark_open' name ('(' name ')')?

    28 \<close>}
    27 Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
    29 Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
    28 Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
    30 Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
    29 The corresponding \texttt{*.fdl} and \texttt{*.rls}
    31 The corresponding \texttt{*.fdl} and \texttt{*.rls}
    30 files must reside in the same directory as the file given as an argument to the command.
    32 files must reside in the same directory as the file given as an argument to the command.
    31 This command also generates records and datatypes for the types specified in the
    33 This command also generates records and datatypes for the types specified in the
    34 Since the full package name currently cannot be determined from the files generated by the
    36 Since the full package name currently cannot be determined from the files generated by the
    35 \SPARK{} Examiner, the command also allows to specify an optional package prefix in the
    37 \SPARK{} Examiner, the command also allows to specify an optional package prefix in the
    36 format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
    38 format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
    37 packages, this is necessary in order for the verification environment to be able to map proof
    39 packages, this is necessary in order for the verification environment to be able to map proof
    38 functions and types defined in Isabelle to their \SPARK{} counterparts.
    40 functions and types defined in Isabelle to their \SPARK{} counterparts.
    39 @{rail "@'spark_proof_functions' ((name '=' term)+)"}
    41 @{rail \<open>

    42   @'spark_proof_functions' ((name '=' term)+)

    43 \<close>}
    40 Associates a proof function with the given name to a term. The name should be the full name
    44 Associates a proof function with the given name to a term. The name should be the full name
    41 of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
    45 of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
    42 This command can be used both inside and outside a verification environment. The latter
    46 This command can be used both inside and outside a verification environment. The latter
    43 variant is useful for introducing proof functions that are shared by several procedures
    47 variant is useful for introducing proof functions that are shared by several procedures
    44 or packages, whereas the former allows the given term to refer to the types generated
    48 or packages, whereas the former allows the given term to refer to the types generated
    45 by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
    49 by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
    46 \texttt{*.fdl} file.
    50 \texttt{*.fdl} file.
    47 @{rail "@'spark_types' ((name '=' type (mapping?))+);
    51 @{rail \<open>
    48 mapping: '('((name '=' nameref)+',')')'"}
    52   @'spark_types' ((name '=' type (mapping?))+)

    53   ;

    54   mapping: '('((name '=' nameref)+',')')'

    55 \<close>}
    49 Associates a \SPARK{} type with the given name with an Isabelle type. This command can
    56 Associates a \SPARK{} type with the given name with an Isabelle type. This command can
    50 only be used outside a verification environment. The given type must be either a record
    57 only be used outside a verification environment. The given type must be either a record
    51 or a datatype, where the names of fields or constructors must either match those of the
    58 or a datatype, where the names of fields or constructors must either match those of the
    52 corresponding \SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle
    59 corresponding \SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle
    53 names has to be provided.
    60 names has to be provided.
    55 proof functions referring to record or enumeration types that are shared by several
    62 proof functions referring to record or enumeration types that are shared by several
    56 procedures or packages. First, the types required by the proof functions can be introduced
    63 procedures or packages. First, the types required by the proof functions can be introduced
    57 using Isabelle's commands for defining records or datatypes. Having introduced the
    64 using Isabelle's commands for defining records or datatypes. Having introduced the
    58 types, the proof functions can be defined in Isabelle. Finally, both the proof
    65 types, the proof functions can be defined in Isabelle. Finally, both the proof
    59 functions and the types can be associated with their \SPARK{} counterparts.
    66 functions and the types can be associated with their \SPARK{} counterparts.
    60 @{rail "@'spark_status' (('(proved)' | '(unproved)')?)"}
    67 @{rail \<open>

    68   @'spark_status' (('(proved)' | '(unproved)')?)

    69 \<close>}
    61 Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
    70 Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
    62 the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
    71 the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
    63 The output can be restricted to the proved or unproved VCs by giving the corresponding
    72 The output can be restricted to the proved or unproved VCs by giving the corresponding
    64 option to the command.
    73 option to the command.
    65 @{rail "@'spark_vc' name"}
    74 @{rail \<open>

    75   @'spark_vc' name

    76 \<close>}
    66 Initiates the proof of the VC with the given name. Similar to the standard
    77 Initiates the proof of the VC with the given name. Similar to the standard
    67 \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
    78 \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
    68 must be followed by a sequence of proof commands. The command introduces the
    79 must be followed by a sequence of proof commands. The command introduces the
    69 hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
    80 hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
    70 \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
    81 \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
    71 @{rail "@'spark_end' '(incomplete)'?"}
    82 @{rail \<open>

    83   @'spark_end' '(incomplete)'?

    84 \<close>}
    72 Closes the current verification environment. Unless the \texttt{incomplete}
    85 Closes the current verification environment. Unless the \texttt{incomplete}
    73 option is given, all VCs must have been proved,
    86 option is given, all VCs must have been proved,
    74 otherwise the command issues an error message. As a side effect, the command
    87 otherwise the command issues an error message. As a side effect, the command
    75 generates a proof review (\texttt{*.prv}) file to inform POGS of the proved
    88 generates a proof review (\texttt{*.prv}) file to inform POGS of the proved
    76 VCs.
    89 VCs.