655 programming language expects these rules as {\em proved} theorems, and |
655 programming language expects these rules as {\em proved} theorems, and |
656 not as axioms implemented in the above brute force manner; otherwise |
656 not as axioms implemented in the above brute force manner; otherwise |
657 all the verification efforts envisaged (like proof of the |
657 all the verification efforts envisaged (like proof of the |
658 post-condition, see below) would be meaningless. |
658 post-condition, see below) would be meaningless. |
659 |
659 |
660 Isabelle provides a large body of knowledge, rigorously proven from |
660 Isabelle provides a large body of knowledge, rigorously proved from |
661 the basic axioms of mathematics~\footnote{This way of rigorously |
661 the basic axioms of mathematics~\footnote{This way of rigorously |
662 deriving all knowledge from first principles is called the |
662 deriving all knowledge from first principles is called the |
663 LCF-paradigm in TP.}. In the case of the ${\cal z}$-Transform the most advanced |
663 LCF-paradigm in TP.}. In the case of the ${\cal z}$-Transform the most advanced |
664 knowledge can be found in the theories on Multivariate |
664 knowledge can be found in the theories on Multivariate |
665 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, |
665 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, |
750 is prepared to get a program, automatically generated by {\sisac} for |
750 is prepared to get a program, automatically generated by {\sisac} for |
751 producing intermediate rewrites when requested by the user. |
751 producing intermediate rewrites when requested by the user. |
752 |
752 |
753 \end{description} |
753 \end{description} |
754 |
754 |
755 \noindent It is advisable to immediately test rule-sets; for that |
755 %OUTCOMMENTED DUE TO SPACE RESTRICTIONS |
756 purpose an appropriate term has to be created; \textit{parse} takes a |
756 % \noindent It is advisable to immediately test rule-sets; for that |
757 context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal |
757 % purpose an appropriate term has to be created; \textit{parse} takes a |
758 Z}^{-1}$) and creates a term: |
758 % context \textit{ctxt} and a string (with \textit{ZZ\_1} denoting ${\cal |
759 |
759 % Z}^{-1}$) and creates a term: |
760 {\footnotesize |
760 % |
761 \begin{verbatim} |
761 % {\footnotesize |
762 01 ML {* |
762 % \begin{verbatim} |
763 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)"; |
763 % 01 ML {* |
764 03 *} |
764 % 02 val t = parse ctxt "ZZ_1 (z / (z - 1) + z / (z - </alpha>) + 1)"; |
765 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1", |
765 % 03 *} |
766 05 "RealDef.real => RealDef.real => RealDef.real") $ |
766 % 04 val t = Const ("Build_Inverse_Z_Transform.ZZ_1", |
767 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...) |
767 % 05 "RealDef.real => RealDef.real => RealDef.real") $ |
768 \end{verbatim}} |
768 % 06 (Const (...) $ (Const (...) $ Free (...) $ (Const (...) $ Free (...) |
769 |
769 % \end{verbatim}} |
770 \noindent The internal representation of the term, as required for |
770 % |
771 rewriting, consists of \textit{Const}ants, a pair of a string |
771 % \noindent The internal representation of the term, as required for |
772 \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables |
772 % rewriting, consists of \textit{Const}ants, a pair of a string |
773 \textit{Free} and the respective constructor \textit{\$}. Now the |
773 % \textit{"Groups.plus\_class.plus"} for $+$ and a type, variables |
774 term can be rewritten by the rule-set \textit{inverse\_z}: |
774 % \textit{Free} and the respective constructor \textit{\$}. Now the |
775 |
775 % term can be rewritten by the rule-set \textit{inverse\_z}: |
776 {\footnotesize |
776 % |
777 \begin{verbatim} |
777 % {\footnotesize |
778 01 ML {* |
778 % \begin{verbatim} |
779 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t; |
779 % 01 ML {* |
780 03 term2str t'; |
780 % 02 val SOME (t', asm) = rewrite_set_ @{theory} inverse\_z t; |
781 04 terms2str asm; |
781 % 03 term2str t'; |
782 05 *} |
782 % 04 terms2str asm; |
783 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string |
783 % 05 *} |
784 07 val it = "|| z || > 1 & || z || > </alpha>" : string |
784 % 06 val it = "u[n] + </alpha> ^ n * u[n] + </delta>[n]" : string |
785 \end{verbatim}} |
785 % 07 val it = "|| z || > 1 & || z || > </alpha>" : string |
786 |
786 % \end{verbatim}} |
787 \noindent The resulting term \textit{t} and the assumptions |
787 % |
788 \textit{asm} are converted to readable strings by \textit{term2str} |
788 % \noindent The resulting term \textit{t} and the assumptions |
789 and \textit{terms2str}. |
789 % \textit{asm} are converted to readable strings by \textit{term2str} |
|
790 % and \textit{terms2str}. |
790 |
791 |
791 \subsection{Preparation of ML-Functions}\label{funs} |
792 \subsection{Preparation of ML-Functions}\label{funs} |
792 Some functionality required in programming, cannot be accomplished by |
793 Some functionality required in programming, cannot be accomplished by |
793 rewriting. So the prototype has a mechanism to call functions within |
794 rewriting. So the prototype has a mechanism to call functions within |
794 the rewrite-engine: certain regexes in Isabelle terms call these |
795 the rewrite-engine: certain redexes in Isabelle terms call these |
795 functions written in SML~\cite{pl:milner97}, the implementation {\em |
796 functions written in SML~\cite{pl:milner97}, the implementation {\em |
796 and} meta-language of Isabelle. The programmer has to use this |
797 and} meta-language of Isabelle. The programmer has to use this |
797 mechanism. |
798 mechanism. |
798 |
799 |
799 In the running example's program on p.\pageref{s:impl} the lines {\rm |
800 In the running example's program on p.\pageref{s:impl} the lines {\rm |
844 | eval_argument_in _ _ _ _ = NONE; |
845 | eval_argument_in _ _ _ _ = NONE; |
845 *} |
846 *} |
846 \end{verbatim}} |
847 \end{verbatim}} |
847 |
848 |
848 \noindent The function body creates either creates \texttt{NONE} |
849 \noindent The function body creates either creates \texttt{NONE} |
849 telling the rewrite-engine to search for the next regex, or creates an |
850 telling the rewrite-engine to search for the next redex, or creates an |
850 ad-hoc theorem for rewriting, thus the programmer needs to adopt many |
851 ad-hoc theorem for rewriting, thus the programmer needs to adopt many |
851 technicalities of Isabelle, for instance, the \textit{Trueprop} |
852 technicalities of Isabelle, for instance, the \textit{Trueprop} |
852 constant. |
853 constant. |
853 |
854 |
854 \bigskip This sub-task particularly sheds light on basic issues in the |
855 \bigskip This sub-task particularly sheds light on basic issues in the |
1297 |
1298 |
1298 The program code, above presented as a string, is parsed by Isabelle's |
1299 The program code, above presented as a string, is parsed by Isabelle's |
1299 parser --- the program is an Isabelle term. This fact is expected to |
1300 parser --- the program is an Isabelle term. This fact is expected to |
1300 simplify verification tasks in the future; on the other hand, this |
1301 simplify verification tasks in the future; on the other hand, this |
1301 fact causes troubles in error detection which are discussed as part |
1302 fact causes troubles in error detection which are discussed as part |
1302 of the workflow in the subsequent section. |
1303 of the work-flow in the subsequent section. |
1303 |
1304 |
1304 \section{Workflow of Programming in the Prototype}\label{workflow} |
1305 \section{Work-flow of Programming in the Prototype}\label{workflow} |
1305 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great |
1306 The new prover IDE Isabelle/jEdit~\cite{makar-jedit-12} is a great |
1306 step forward for interactive theory and proof development. The |
1307 step forward for interactive theory and proof development. The |
1307 {\sisac}-prototype re-uses this IDE as a programming environment. The |
1308 {\sisac}-prototype re-uses this IDE as a programming environment. The |
1308 experiences from this re-use show, that the essential components are |
1309 experiences from this re-use show, that the essential components are |
1309 available from Isabelle/jEdit. However, additional tools and features |
1310 available from Isabelle/jEdit. However, additional tools and features |
1366 \noindent The resulting term \texttt{t'} is \texttt{Free ("z", |
1367 \noindent The resulting term \texttt{t'} is \texttt{Free ("z", |
1367 "RealDef.real")}, i.e the variable \texttt{z}, so all is |
1368 "RealDef.real")}, i.e the variable \texttt{z}, so all is |
1368 perfect. Probably we have forgotten to store this function correctly~? |
1369 perfect. Probably we have forgotten to store this function correctly~? |
1369 We review the respective \texttt{calclist} (again an |
1370 We review the respective \texttt{calclist} (again an |
1370 \textit{Unsynchronized.ref} to be removed in order to adjust to |
1371 \textit{Unsynchronized.ref} to be removed in order to adjust to |
1371 IsabelleIsar's asynchronous document model): |
1372 Isabelle/Isar's asynchronous document model): |
1372 |
1373 |
1373 {\footnotesize |
1374 {\footnotesize |
1374 \begin{verbatim} |
1375 \begin{verbatim} |
1375 calclist:= overwritel (! calclist, |
1376 calclist:= overwritel (! calclist, |
1376 [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), |
1377 [("argument_in",("Build_Inverse_Z_Transform.argument'_in", eval_argument_in "")), |
1399 however, is not meant for huge terms like the program of the running |
1400 however, is not meant for huge terms like the program of the running |
1400 example. So reading out the specific error (usually type errors) from |
1401 example. So reading out the specific error (usually type errors) from |
1401 Isabelle's message is difficult. |
1402 Isabelle's message is difficult. |
1402 |
1403 |
1403 \medskip Testing the evaluation of the program has to rely on very |
1404 \medskip Testing the evaluation of the program has to rely on very |
1404 simple tools. Step-wise execution is modelled by a function |
1405 simple tools. Step-wise execution is modeled by a function |
1405 \texttt{me}, short for mathematics-engine~\footnote{The interface used |
1406 \texttt{me}, short for mathematics-engine~\footnote{The interface used |
1406 by the fron-end which created the calculation on |
1407 by the front-end which created the calculation on |
1407 p.\pageref{fig-interactive} is different from this function}: |
1408 p.\pageref{fig-interactive} is different from this function}: |
1408 %the following is a simplification of the actual function |
1409 %the following is a simplification of the actual function |
1409 |
1410 |
1410 {\footnotesize |
1411 {\footnotesize |
1411 \begin{verbatim} |
1412 \begin{verbatim} |
1887 A brief re-introduction of the novel kind of programming |
1888 A brief re-introduction of the novel kind of programming |
1888 language by example of the {\sisac}-prototype makes the paper |
1889 language by example of the {\sisac}-prototype makes the paper |
1889 self-contained. The main section describes all the main concepts |
1890 self-contained. The main section describes all the main concepts |
1890 involved in TP-based programming and all the sub-tasks concerning |
1891 involved in TP-based programming and all the sub-tasks concerning |
1891 respective implementation: mechanisation of mathematics and domain |
1892 respective implementation: mechanisation of mathematics and domain |
1892 modelling, implementation of term rewriting systems for the |
1893 modeling, implementation of term rewriting systems for the |
1893 rewriting-engine, formal (implicit) specification of the problem to be |
1894 rewriting-engine, formal (implicit) specification of the problem to be |
1894 (explicitly) described by the program, implementation of the many components |
1895 (explicitly) described by the program, implementation of the many components |
1895 required for Lucas-Interpretation and finally implementation of the |
1896 required for Lucas-Interpretation and finally implementation of the |
1896 program itself. |
1897 program itself. |
1897 |
1898 |
1898 The many concepts and sub-tasks involved in programming require a |
1899 The many concepts and sub-tasks involved in programming require a |
1899 comprehensive workflow; first experiences with the workflow as |
1900 comprehensive work-flow; first experiences with the work-flow as |
1900 supported by the present prototype are described as well: Isabelle + |
1901 supported by the present prototype are described as well: Isabelle + |
1901 Isar + jEdit provide appropriate components for establishing an |
1902 Isar + jEdit provide appropriate components for establishing an |
1902 efficient development environment integrating computation and |
1903 efficient development environment integrating computation and |
1903 deduction. However, the present state of the prototype is far off a |
1904 deduction. However, the present state of the prototype is far off a |
1904 state appropriate for wide-spread use: the prototype of the program |
1905 state appropriate for wide-spread use: the prototype of the program |