1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Sep 13 22:44:56 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Fri Sep 14 12:23:39 2012 +0200
1.3 @@ -105,7 +105,7 @@
1.4 \textit{Jan Ro\v{c}nik} \\
1.5 jan.rocnik@student.tugraz.at \\
1.6 IST, SPSC\\
1.7 -Graz University of Technologie\\
1.8 +Graz University of Technology\\
1.9 Austria\end{tabular}
1.10 }%
1.11 %
1.12 @@ -657,7 +657,7 @@
1.13 all the verification efforts envisaged (like proof of the
1.14 post-condition, see below) would be meaningless.
1.15
1.16 -Isabelle provides a large body of knowledge, rigorously proven from
1.17 +Isabelle provides a large body of knowledge, rigorously proved from
1.18 the basic axioms of mathematics~\footnote{This way of rigorously
1.19 deriving all knowledge from first principles is called the
1.20 LCF-paradigm in TP.}. In the case of the ${\cal z}$-Transform the most advanced
1.21 @@ -752,46 +752,47 @@
1.22
1.23 \end{description}
1.24
1.25 -\noindent It is advisable to immediately test rule-sets; for that
1.26 -purpose an appropriate term has to be created; \textit{parse} takes a
1.27 -context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
1.28 -Z}^{-1}$) and creates a term:
1.29 -
1.30 -{\footnotesize
1.31 -\begin{verbatim}
1.32 - 01 ML {*
1.33 - 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
1.34 - 03 *}
1.35 - 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
1.36 - 05 "RealDef.real => RealDef.real => RealDef.real") $
1.37 - 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
1.38 -\end{verbatim}}
1.39 -
1.40 -\noindent The internal representation of the term, as required for
1.41 -rewriting, consists of \textit{Const}ants, a pair of a string
1.42 -\textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
1.43 -\textit{Free} and the respective constructor \textit{\$}. Now the
1.44 -term can be rewritten by the rule-set \textit{inverse\_z}:
1.45 -
1.46 -{\footnotesize
1.47 -\begin{verbatim}
1.48 - 01 ML {*
1.49 - 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
1.50 - 03 term2str t';
1.51 - 04 terms2str asm;
1.52 - 05 *}
1.53 - 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
1.54 - 07 val it = "|| z || > 1 & || z || > </alpha>" : string
1.55 -\end{verbatim}}
1.56 -
1.57 -\noindent The resulting term \textit{t} and the assumptions
1.58 -\textit{asm} are converted to readable strings by \textit{term2str}
1.59 -and \textit{terms2str}.
1.60 +%OUTCOMMENTED DUE TO SPACE RESTRICTIONS
1.61 +% \noindent It is advisable to immediately test rule-sets; for that
1.62 +% purpose an appropriate term has to be created; \textit{parse} takes a
1.63 +% context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal
1.64 +% Z}^{-1}$) and creates a term:
1.65 +%
1.66 +% {\footnotesize
1.67 +% \begin{verbatim}
1.68 +% 01 ML {*
1.69 +% 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)";
1.70 +% 03 *}
1.71 +% 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1",
1.72 +% 05 "RealDef.real => RealDef.real => RealDef.real") $
1.73 +% 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...)
1.74 +% \end{verbatim}}
1.75 +%
1.76 +% \noindent The internal representation of the term, as required for
1.77 +% rewriting, consists of \textit{Const}ants, a pair of a string
1.78 +% \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables
1.79 +% \textit{Free} and the respective constructor \textit{\$}. Now the
1.80 +% term can be rewritten by the rule-set \textit{inverse\_z}:
1.81 +%
1.82 +% {\footnotesize
1.83 +% \begin{verbatim}
1.84 +% 01 ML {*
1.85 +% 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t;
1.86 +% 03 term2str t';
1.87 +% 04 terms2str asm;
1.88 +% 05 *}
1.89 +% 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string
1.90 +% 07 val it = "|| z || > 1 & || z || > </alpha>" : string
1.91 +% \end{verbatim}}
1.92 +%
1.93 +% \noindent The resulting term \textit{t} and the assumptions
1.94 +% \textit{asm} are converted to readable strings by \textit{term2str}
1.95 +% and \textit{terms2str}.
1.96
1.97 \subsection{Preparation of ML-Functions}\label{funs}
1.98 Some functionality required in programming, cannot be accomplished by
1.99 rewriting. So the prototype has a mechanism to call functions within
1.100 -the rewrite-engine: certain regexes in Isabelle terms call these
1.101 +the rewrite-engine: certain redexes in Isabelle terms call these
1.102 functions written in SML~\cite{pl:milner97}, the implementation {\em
1.103 and} meta-language of Isabelle. The programmer has to use this
1.104 mechanism.
1.105 @@ -846,7 +847,7 @@
1.106 \end{verbatim}}
1.107
1.108 \noindent The function body creates either creates \texttt{NONE}
1.109 -telling the rewrite-engine to search for the next regex, or creates an
1.110 +telling the rewrite-engine to search for the next redex, or creates an
1.111 ad-hoc theorem for rewriting, thus the programmer needs to adopt many
1.112 technicalities of Isabelle, for instance, the \textit{Trueprop}
1.113 constant.
1.114 @@ -1299,9 +1300,9 @@
1.115 parser --- the program is an Isabelle term. This fact is expected to
1.116 simplify verification tasks in the future; on the other hand, this
1.117 fact causes troubles in error detection which are discussed as part
1.118 -of the workflow in the subsequent section.
1.119 +of the work-flow in the subsequent section.
1.120
1.121 -\section{Workflow of Programming in the Prototype}\label{workflow}
1.122 +\section{Work-flow of Programming in the Prototype}\label{workflow}
1.123 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great
1.124 step forward for interactive theory and proof development. The
1.125 {\sisac}-prototype re-uses this IDE as a programming environment. The
1.126 @@ -1368,7 +1369,7 @@
1.127 perfect. Probably we have forgotten to store this function correctly~?
1.128 We review the respective \texttt{calclist} (again an
1.129 \textit{Unsynchronized.ref} to be removed in order to adjust to
1.130 -IsabelleIsar's asynchronous document model):
1.131 +Isabelle/Isar's asynchronous document model):
1.132
1.133 {\footnotesize
1.134 \begin{verbatim}
1.135 @@ -1401,9 +1402,9 @@
1.136 Isabelle's message is difficult.
1.137
1.138 \medskip Testing the evaluation of the program has to rely on very
1.139 -simple tools. Step-wise execution is modelled by a function
1.140 +simple tools. Step-wise execution is modeled by a function
1.141 \texttt{me}, short for mathematics-engine~\footnote{The interface used
1.142 -by the fron-end which created the calculation on
1.143 +by the front-end which created the calculation on
1.144 p.\pageref{fig-interactive} is different from this function}:
1.145 %the following is a simplification of the actual function
1.146
1.147 @@ -1889,14 +1890,14 @@
1.148 self-contained. The main section describes all the main concepts
1.149 involved in TP-based programming and all the sub-tasks concerning
1.150 respective implementation: mechanisation of mathematics and domain
1.151 -modelling, implementation of term rewriting systems for the
1.152 +modeling, implementation of term rewriting systems for the
1.153 rewriting-engine, formal (implicit) specification of the problem to be
1.154 (explicitly) described by the program, implementation of the many components
1.155 required for Lucas-Interpretation and finally implementation of the
1.156 program itself.
1.157
1.158 The many concepts and sub-tasks involved in programming require a
1.159 -comprehensive workflow; first experiences with the workflow as
1.160 +comprehensive work-flow; first experiences with the work-flow as
1.161 supported by the present prototype are described as well: Isabelle +
1.162 Isar + jEdit provide appropriate components for establishing an
1.163 efficient development environment integrating computation and
1.164 @@ -1946,4 +1947,12 @@
1.165 \bibliographystyle{alpha}
1.166 {\small\bibliography{references}}
1.167
1.168 -\end{document}
1.169 \ No newline at end of file
1.170 +\end{document}
1.171 +% LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
1.172 +% LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised
1.173 +% LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
1.174 +% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
1.175 +% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
1.176 +% LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq
1.177 +% LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
1.178 +% LocalWords: mechanisation multi