1073 fact causes troubles in error detectetion which are discussed as part |
1073 fact causes troubles in error detectetion which are discussed as part |
1074 of the workflow in the subsequent section. |
1074 of the workflow in the subsequent section. |
1075 |
1075 |
1076 \section{Workflow of Programming in the Prototype}\label{workflow} |
1076 \section{Workflow of Programming in the Prototype}\label{workflow} |
1077 The previous section presented all the duties and tasks to be accomplished by |
1077 The previous section presented all the duties and tasks to be accomplished by |
1078 programmers of TP-based languages. The tasks are interrelated |
1078 programmers of TP-based languages. Some tasks are interrelated and comprehensive, |
|
1079 so first experiences with the workflow in programming are noted below. The notes |
|
1080 also capture requirements for future language development. |
1079 |
1081 |
1080 \subsection{Preparations and Trials}\label{flow-prep} |
1082 \subsection{Preparations and Trials}\label{flow-prep} |
1081 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions'' |
1083 % Build\_Inverse\_Z\_Transform.thy ... ``imports PolyEq DiffApp Partial\_Fractions'' |
|
1084 The new graphical user-interface of Isabelle~\cite{makar-jedit-12} is a great |
|
1085 step forward for interactive theory and proof development --- and so it is for |
|
1086 interactive program development; the specific requirements raised by interactive |
|
1087 programming will be mentioned separately. |
|
1088 |
|
1089 The development in the {\sisac}-prototype was done in a separate |
|
1090 theory~\footnote{http://www.ist.tugraz.at/projects/isac/publ/Build\_Inverse\_Z\_Transform.thy}. |
|
1091 The workflow tackled the tasks more or less following the order of the |
|
1092 above sections from \S\ref{isabisac} to \S\ref{funs}. At each stage the |
|
1093 interactivity of Isabelle/jEdit is very supportive. For instance, as soon as the |
|
1094 theorems for the Z-transform are established (see \S\ref{isabisac}) it is tempting |
|
1095 to see them at work: |
|
1096 |
|
1097 |
|
1098 |
1082 .\\.\\.\\ |
1099 .\\.\\.\\ |
1083 |
1100 |
1084 %JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich |
1101 %JR: Hier sollte eigentlich stehen was nun bei 4.3.1 ist. Habe das erst kürzlich |
1085 %JR: eingefügt; das war der beinn unserer Arbeit in |
1102 %JR: eingefügt; das war der beinn unserer Arbeit in |
1086 %JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei |
1103 %JR: Build_Inverse_Z_Transformation und beschreibt die meiner Meinung nach bei |
1147 |
1164 |
1148 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} |
1165 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} |
1149 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ? |
1166 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ? |
1150 |
1167 |
1151 |
1168 |
1152 |
1169 http://www.ist.tugraz.at/projects/isac/publ/Inverse\_Z\_Transform.thy |
1153 |
1170 |
1154 % \newpage |
1171 % \newpage |
1155 % ------------------------------------------------------------------- |
1172 % ------------------------------------------------------------------- |
1156 % |
1173 % |
1157 % Material, falls noch Platz bleibt ... |
1174 % Material, falls noch Platz bleibt ... |