800 {\footnotesize |
800 {\footnotesize |
801 \begin{verbatim} |
801 \begin{verbatim} |
802 01 val inverse_z = Rls |
802 01 val inverse_z = Rls |
803 02 {id = "inverse_z", |
803 02 {id = "inverse_z", |
804 03 rew_ord = dummy_ord, |
804 03 rew_ord = dummy_ord, |
805 04 erls = Erls, |
805 04 asm_rls = Erls, |
806 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), |
806 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), |
807 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), |
807 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), |
808 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})], |
808 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})], |
809 08 errpatts = [], |
809 08 errpatts = [], |
810 09 scr = ""} |
810 09 program = ""} |
811 \end{verbatim}} |
811 \end{verbatim}} |
812 |
812 |
813 \noindent The items, line by line, in the above record have the following purpose: |
813 \noindent The items, line by line, in the above record have the following purpose: |
814 \begin{description} |
814 \begin{description} |
815 \item[01..02] the ML-value \textit{inverse\_z} stores it's identifier |
815 \item[01..02] the ML-value \textit{inverse\_z} stores it's identifier |
817 layers of Isabelle/ML (like in the Lucas-Interpreter) and |
817 layers of Isabelle/ML (like in the Lucas-Interpreter) and |
818 Isabelle/Isar (like in the example program on p.\pageref{s:impl} on |
818 Isabelle/Isar (like in the example program on p.\pageref{s:impl} on |
819 line {\rm 12}). |
819 line {\rm 12}). |
820 |
820 |
821 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that} |
821 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that} |
822 \textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here: |
822 \textit{rew\_ord} and (b) the rule-set \textit{asm_rls} are trivial here: |
823 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting |
823 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting |
824 and (b) the assumptions of the \textit{rules} need not be evaluated |
824 and (b) the assumptions of the \textit{rules} need not be evaluated |
825 (they just go into the context during rewriting). |
825 (they just go into the context during rewriting). |
826 |
826 |
827 \item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1}; |
827 \item[05..07] the \textit{rules} are the axioms from p.\pageref{eg:neuper1}; |
828 also ML-functions (\S\ref{funs}) can come into this list as shown in |
828 also ML-functions (\S\ref{funs}) can come into this list as shown in |
829 \S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm} |
829 \S\ref{flow-prep}; so they are distinguished by type-constructors \textit{Thm} |
830 and \textit{Calc} respectively; for the purpose of reflection both |
830 and \textit{Calc} respectively; for the purpose of reflection both |
831 contain their identifiers. |
831 contain their identifiers. |
832 |
832 |
833 \item[08..09] are error-patterns not discussed here and \textit{scr} |
833 \item[08..09] are error-patterns not discussed here and \textit{program} |
834 is prepared to get a program, automatically generated by {\sisac} for |
834 is prepared to get a program, automatically generated by {\sisac} for |
835 producing intermediate rewrites when requested by the user. |
835 producing intermediate rewrites when requested by the user. |
836 |
836 |
837 \end{description} |
837 \end{description} |
838 |
838 |
1107 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], |
1107 06 ( ["Inverse", "Z_Transform", "SignalProcessing"], |
1108 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), |
1108 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), |
1109 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), |
1109 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), |
1110 09 ("#Find" , ["stepResponse n_eq"]), |
1110 09 ("#Find" , ["stepResponse n_eq"]), |
1111 10 ("#Post" , [" TODO "])]) |
1111 10 ("#Post" , [" TODO "])]) |
1112 11 prls |
1112 11 where_rls |
1113 12 NONE |
1113 12 NONE |
1114 13 [["SignalProcessing","Z_Transform","Inverse"]]); |
1114 13 [["SignalProcessing","Z_Transform","Inverse"]]); |
1115 14 *} |
1115 14 *} |
1116 \end{verbatim}} |
1116 \end{verbatim}} |
1117 |
1117 |
1161 % TODO: search generalized for subthy (ref.p.69*) |
1161 % TODO: search generalized for subthy (ref.p.69*) |
1162 % (*^^^ WN050912 NOT used during application of the problem, |
1162 % (*^^^ WN050912 NOT used during application of the problem, |
1163 % because applied terms may be from 'subthy' as well as from super; |
1163 % because applied terms may be from 'subthy' as well as from super; |
1164 % thus we take 'maxthy'; see match_ags !*) |
1164 % thus we take 'maxthy'; see match_ags !*) |
1165 % cas : term option,(*'CAS-command'*) |
1165 % cas : term option,(*'CAS-command'*) |
1166 % prls : rls, (* for preds in where_*) |
1166 % where_rls : rls, (* for preds in where_*) |
1167 % where_: term list, (* where - predicates*) |
1167 % where_: term list, (* where - predicates*) |
1168 % ppc : pat list, |
1168 % model : pat list, |
1169 % (*this is the model-pattern; |
1169 % (*this is the model-pattern; |
1170 % it contains "#Given","#Where","#Find","#Relate"-patterns |
1170 % it contains "#Given","#Where","#Find","#Relate"-patterns |
1171 % for constraints on identifiers see "fun copy_name"*) |
1171 % for constraints on identifiers see "fun copy_name"*) |
1172 % met : metID list}; (* methods solving the pbt*) |
1172 % met : metID list}; (* methods solving the pbt*) |
1173 % |
1173 % |
1223 05 thy |
1223 05 thy |
1224 06 ( ["SignalProcessing", "Z_Transform", "Inverse"], |
1224 06 ( ["SignalProcessing", "Z_Transform", "Inverse"], |
1225 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), |
1225 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), |
1226 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), |
1226 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), |
1227 09 ("#Find" , ["stepResponse n_eq"]), |
1227 09 ("#Find" , ["stepResponse n_eq"]), |
1228 10 rew_ord erls |
1228 10 rew_ord asm_rls |
1229 11 srls prls nrls |
1229 11 prog_rls where_rls rew_rls |
1230 12 errpats |
1230 12 errpats |
1231 13 program); |
1231 13 program); |
1232 14 *} |
1232 14 *} |
1233 \end{verbatim}} |
1233 \end{verbatim}} |
1234 |
1234 |
1242 {\em guard}: as long as not all \textit{Given} items are present and |
1242 {\em guard}: as long as not all \textit{Given} items are present and |
1243 the \textit{Pre}-conditions is not true, interpretation of the program |
1243 the \textit{Pre}-conditions is not true, interpretation of the program |
1244 is not started. |
1244 is not started. |
1245 |
1245 |
1246 \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case |
1246 \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case |
1247 \textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets |
1247 \textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{asm_rls} features evaluating the conditions. The rule-sets |
1248 \textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g. |
1248 \textit{prog_rls, where_rls, rew_rls} feature evaluating (a) the ML-functions in the program (e.g. |
1249 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec} |
1249 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec} |
1250 and (c) is required for the derivation-machinery checking user-input formulas. |
1250 and (c) is required for the derivation-machinery checking user-input formulas. |
1251 |
1251 |
1252 \item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}. |
1252 \item[12..13] \textit{errpats} are error-patterns~\cite{gdaroczy-EP-13} for this method and \textit{program} is the variable holding the example from p.\pageref {s:impl}. |
1253 \end{description} |
1253 \end{description} |
1464 05 ]);\end{verbatim}} |
1464 05 ]);\end{verbatim}} |
1465 |
1465 |
1466 \noindent The entry is perfect. So what is the reason~? Ah, probably there |
1466 \noindent The entry is perfect. So what is the reason~? Ah, probably there |
1467 is something messed up with the many rule-sets in the method, see \S\ref{meth} --- |
1467 is something messed up with the many rule-sets in the method, see \S\ref{meth} --- |
1468 right, the function \texttt{argument\_in} is not contained in the respective |
1468 right, the function \texttt{argument\_in} is not contained in the respective |
1469 rule-set \textit{srls} \dots this just as an example of the intricacies in |
1469 rule-set \textit{prog_rls} \dots this just as an example of the intricacies in |
1470 debugging a program in the present state of the prototype. |
1470 debugging a program in the present state of the prototype. |
1471 |
1471 |
1472 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} |
1472 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} |
1473 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth}, |
1473 Given all the prerequisites from \S\ref{isabisac} to \S\ref{meth}, |
1474 usually developed within several iterations, the program can be |
1474 usually developed within several iterations, the program can be |
2126 |
2126 |
2127 \end{document} |
2127 \end{document} |
2128 % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley |
2128 % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley |
2129 % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised |
2129 % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised |
2130 % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML |
2130 % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML |
2131 % LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls |
2131 % LocalWords: recognised hoc Trueprop redexes Unsynchronized where_ rhs ord asm_rls |
2132 % LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs |
2132 % LocalWords: prog_rls where_rls rew_rls lhs errpats InverseZTransform SubProblem IDE IDEs |
2133 % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq |
2133 % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq |
2134 % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's |
2134 % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's |
2135 % LocalWords: mechanisation multi |
2135 % LocalWords: mechanisation multi |