equal
deleted
inserted
replaced
47 environment must import the theory \texttt{SPARK}. In addition, we also include |
47 environment must import the theory \texttt{SPARK}. In addition, we also include |
48 the \texttt{GCD} theory. The list of imported theories is followed by the |
48 the \texttt{GCD} theory. The list of imported theories is followed by the |
49 \isa{\isacommand{begin}} keyword. In order to interactively process the theory |
49 \isa{\isacommand{begin}} keyword. In order to interactively process the theory |
50 shown in \figref{fig:gcd-proof}, we start Isabelle with the command |
50 shown in \figref{fig:gcd-proof}, we start Isabelle with the command |
51 \begin{verbatim} |
51 \begin{verbatim} |
52 isabelle emacs -l HOL-SPARK Greatest_Common_Divisor.thy |
52 isabelle jedit -l HOL-SPARK Greatest_Common_Divisor.thy |
53 \end{verbatim} |
53 \end{verbatim} |
54 The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right |
54 The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right |
55 object logic image containing the verification environment. Each proof function |
55 object logic image containing the verification environment. Each proof function |
56 occurring in the specification of a \SPARK{} program must be linked with a |
56 occurring in the specification of a \SPARK{} program must be linked with a |
57 corresponding Isabelle function. This is accomplished by the command |
57 corresponding Isabelle function. This is accomplished by the command |