1 %nicht vergessen: auch srd.tex ($Revision $) \"andern !
2 \chapter{Software Requirements Document}
4 This Software Requirements Document is structured along the modules
5 abstracted from the functionality defined in the User Requirements
6 Document. The User Requirements Document, however, is structured along
7 the different kinds of users envisaged. In order to establish
8 comfortable tracing, the $m:n$ relation between user requirements and
9 software requirements will be accurrately recorded in a double-linked
12 \section{General requirements}
13 %One goal of this section is to achieve a smooth design and minimize the effort in development. Although \sisac consists of a number of (more or less) autonomous modules, a number of developments can be shared.
15 \subparagraph{Delopment environment,} standards and components, documentation and revision control are described in appendix \ref{AP:environment}.
17 \subparagraph{The call hierarchy} between the components underlies a severe restriction due to UR \ref{access-ab} and UR \ref{isac-www}: Because a browser can only deliver a HTTP-request, the worksheet must start browsers, too (and not only the dialog, as it would be desirable w.r.t. the system architecture).
18 {\bf\SR Browsers are called by a 'master-browser' {\em and} by the worksheet. \label{}} ??? %WN2.12.02 ...... ausbessern !!!!
20 \subparagraph{The connection between Java and SML} has to be 'hand-made'. During the next few years there will be several changes at the interfaces between the
21 \sisac-components belonging to these two language environments.
22 {\bf\SR The SML-kernel is started by a java thread \label{}} which controls the time-out eventuall resulting from non-terminating loops in the knowledge interpreter.
23 {\bf\SR The SML standard-output channel is read by parsers, \label{}} one for the SML-structures, and one for the mathematics formulas embedded in the SML-structures.
25 \subparagraph{System requirements for the users:} Users (with exception of the math authors, which work directly on the SML-kernel) are expected to work on standard-browsers (UR \ref{browser}) and some additional software components.
26 {\bf\SR On the client-side a Java virtual machine version .... \label{}} must reside on the local computer of the learners and authors.
27 {\bf\SR On the server there is a Linux or Unix \label{}} operating system, Linux version ..., Unix ...
31 \section{The worksheet}
32 A worksheet is the protocol of a more or less interactive calculation of an example, and it offers access to all services necessary to calculate the result of the example.
34 \subparagraph{A calculation mirrors the structure of the prooftree.}
35 {\bf\SR The structure of a calculation is given by the ME. \label{}} Consequently any editing in a calculation affects the parts depending on the edited formula or tactic. Edit the worksheet w.r.t. UR \ref{edit} for publication etc. is done outside \sisac{} after having exported the calculation.
36 {\bf\SR Export a calculation to a standard format \label{}} preferably XML plus MathML.
41 \section{The browser generators}
42 \sisac's mathematics knowledge (on (1)theories (2)problems (3)methods)
43 is held in SML datastructures. Here we describe all requirements
44 concerning the generation of the browsers written in Java, whereas
45 the generation of the math knowledge itself is described in the
46 'interfaces for authors of math knowledge'.
48 The browser generators provide the contents for the browsers. This
49 means that a browser querys its respective browser generator about
50 subnodes etc. whereas the further description is held outside the
51 SML-engine. To maintain this connection, unique identifyer are needed.
52 {\bf\SR browser-generators use locally unique identifyers \label{}} (locally unique within SML) for their informations (for each node of their structure).
54 \subparagraph{Data are structured hierarchically,} i.e. the problems, methods and examples. (The theories for a directed graph without cycles; thus it also can presented by a hierarchy.)
55 {\bf\SR The hiearchy displayed in a frame \label{}} in order to have it visible all the time.
56 {\bf\SR The hierarchy has arbitrary levels. \label{}} For the headlines for each level see SR \dots SR \ref{expl-headlines}.
57 {\bf\SR The hierarchy shows the position \label{}} of the related element displayed in the browser-window; for this purpose an additional button is required, because the 'back' and 'forward'-button on the browser may disconnect the relation.
60 \subsection{The theory browser generator}
61 The generation of the theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
62 {\bf\SR The theory browser generator is given by Isabelle. \label{gen-isa}}
64 \subsection{The problem and method browser generators}
67 \subsection{The example browser generator}
68 This authoring component comprises all tools necessary to generate the content displayed by the example browser.
70 {\bf\SR The headlines of the example-hierarchy: \label{expl-headlines}} The hierarchy comprises the labels of the chapters, sections, subsections etc. plus the respective head line, and the blocks of examples with the respective labels -- all defined by the user (see UR \ref{UR161a}).
72 {\bf\SR Integrated editors for text, formulas and figures. \label{}} This integration should be as smooth as possible; it includes an MathML-based formula-editor for the formalization.
74 \section{The knowledge browsers}
76 %W.N.: dieser Abschnitt ist f''ur A.G. + W.N.
77 All browsers (Example-Browser and Knowledge-Browsers) present their
78 output in a similar way. Textual descriptions have to be combined with
79 images, formulas, formalisations, problems, \dots and links to further
80 informations(UR\ref{URinterlink}). The structure of this informations
81 has to be taken from the respective browser-generators. All kinds of
82 information might be interlinked among each other, but not all parts
83 of the information might be already present in the system when a new
84 item is inserted. (e.g. a example might use the keyword
85 \emph{is\_rooteq\_in} in its \emph{where}\/clause before the keyword
86 is described in the system. If the example is viewed after a
87 description became available, a link to the explanation should be
88 provided automatically.) To support this feature, the browsers need a
89 fast way to look up a special description.
90 {\bf\SR fast look up for description (includes resolve of the
91 identifyer and query for a description)}
93 \subparagraph{Groups of users} are usually 1-to-1 related to courses; members of courses get specific examples and specific advice by explanations.
94 {\bf\SR Each user is assigned exactly one group during a session. \label{}} The user, however, may start another session as a member of another group.
95 {\bf\SR There is a default group for visitors. \label{}}
98 \subparagraph{Additional data and visibility properties:} A considerable part of the data are additional to the data generated from the SML structures. The visibility concerns enabled or disabled links from problem and methods, and the access to examples from the hierarchy frame. There are respective time constraints on the visibility.
99 {\bf\SR Additional data and visibility are course specific. \label{}}
100 {\bf\SR Time constraints are given by intervals; \label{}} there are specific values for the limits of the interval indicanting infinity (contraint is given from the very beginning, or lasts forever).
103 \subsection{The theory browser}
104 The theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
105 {\bf\SR the theory browser is given by Isabelle. \label{}}
107 \subsection{The problem and method browsers}
108 %\subparagraph{Static and dynamic views onto the KB} are provided by both browsers. Thus the (HTML-) presentation is generated dynamically. The dynamic view for problemjs concerns instantiation by a model of the current calculation on the worksheet. The dynamic view for methods concerns marking the tactic currently applied in a calculation.
109 %{\bf\SR Browsers create the presentation in browser-windows dynamically. \label{}}
111 \subparagraph{Additional data} are explanations and typical examples which may be provided for each problem and each method. Both of these kinds of additional data are spcific for courses and may underly time constraints (UR \ref{expl-locked}, UR \ref{invisible}, UR \ref{restrict-know}).
113 The primary contents are the respective problem and the respective method; {\em all} other data are reachable by links. This holds for special mathematical data (on rulesets etc.) from SML, too.
114 {\bf\SR A problem-page consists of \label{problem-page}} the
116 12345\=123\=123\=\kill
117 \>name of the problem\\
118 \>the fields 'given', 'where', 'find' and 'relate'\\
119 \>a link to the special math data\\
120 \>a list of subordinated methods (only displayed in the hierarchy-frame)\\
121 \>an arbitrary list of links to additional data
123 The next lower and next higher level in the hierarchy can be found in the hierarchy-frame.
124 {\bf\SR A method-page consists of \label{method-page}}
126 12345\=123\=123\=\kill
127 \>name of the method\\
129 \>a link to the special math data\\
130 \>a list of subordinated methods (only displayed in the hierarchy-frame)\\
131 \>an arbitrary list of links to additional data
133 {\bf\SR The links to additional data \label{}} have the following attributes:
135 12345\=123\=123\=\kill
137 \>the reference (to an explanation or to an example starting a worksheet)\\
139 \>\>ID of first group\\
140 \>\>\>locked: list of intervals\\
141 \>\>\>???used by userID ---$>$ usermodel???\\
142 \>\>ID of second group \dots
144 %{\bf\SR Explanations and examples are optional. \label{}} For each problem and each method there is {\em one ???} link for the explanations and {\em one} link for the examples (which may be disabled).
145 %{\bf\SR Access to explanations and examples of other courses \label{}} is possible by ... ??? (see UR \ref{other-courses}).
150 \subsection{The example browser}
151 In contrary to the problem and method browsers, the presentation of the contents of a browser-window is {\em not} generated automatically. UR \ref{expl-layout} requests for a layout 'handmade' by the course designer; there are, however, a lot of attributes invisible for the learner to be added by the course designer, too.
153 \subparagraph{Attributes of examples and collections} are numerous, and thus defaults help to safe space. There is only one collection, partitioned hierarchically into subcollections.
154 {\bf\SR Default data \label{}} are filled in bottum up: A default is filled by the first non-default parent.
155 {\bf\SR A subcollection has the attributes \label{coll-attr}}
157 12345\=123\=123\=123\=123\=\kill
158 \>headline of the collection (displayed also in the hiearchy-frame) \\
159 \>description of the collection\\
160 \>list of subcollections\\
162 \>layout of examples belonging to this subcollection\\
165 \>groups of users, for each group: \\
166 \>\>ID of the group \\
177 \>\>invisible: list of intervals OR duration (? TODO !)\\
178 \>\>locked: list of intervalsOR duration (? TODO !) \\
180 \>\>\>TODO: difficulty, length, \dots \\
181 \>\>\>finished-by: \\
182 \>\>\>\>elements: list of mandatory examples (or groups) to be done \\
183 \>\>\>\>number: number of (arbitrary) examples (or groups) to be done \\
184 \>\>\>\>points: calculated from TODO: difficulty, length, \dots \\
186 Pay attention to the entry 'list of subcollections OR ayout of examples belonging to this subcollection': This means that the subcollection {\em exactly one} hierarchy-level above the bottom of individual examples has a specific content, the graphical layout of the examples. This is in order to meet UR \ref{expl-layout}.
189 {\bf\SR An example has the attributes \label{expl-att}}
191 12345\=123\=123\=123\=123\=123\=\kill
193 \>reference ??? to the description of the example (in the layout ?)\\
194 \>list of formalizations and specifications \\
198 \>groups of users, for each group: \\
199 \>\>ID of the group \\
210 \>\>invisible: list of intervals OR duration (? TODO !) \\
211 \>\>locked: list of intervals OR duration (? TODO !)\\
213 \>\>\>TODO: difficulty, length, \dots \\
214 \>\>???done by userID ---$>$ usermodel???
216 {\bf\SR Hitting the label of the example starts the calculation. \label{}}
218 \subparagraph{Visibility of the examples} is defined in two levels: (1) 'locked' displays the text of the example, but doesn't allow to calculate it; and (2) 'invisible' desn't display the example at all.
219 {\bf\SR {\em Only} visible examples are checked for being locked.\label{}}
220 %{\bf\SR Authoring-/learner-mode:} the formalization and other attributes are shown/not shown, depending on the group the user belongs to.
227 \section{The dialog guide}
229 %{\bf\SR A learner has a dialog state within the current session. \label{}}
230 %{\bf\SR Each learner has a history of all sessions. \label{}}
231 %{\bf\SR The history holds the condensed performance in calculations. \label{}}
232 %{\bf\SR The history holds requests into the knowledge. \label{}\\}
236 As already mentioned, the dialog guide will be fleshed out in a later phase of development involving didactics and learning theory. Now we try to establish a framework open for later completion.
238 \subparagraph{The dialogstate} is read and updated during {\em one} session. A dialog resumes the dialogstate from the previous session done as a member of the same student-group.
239 {\bf\SR The last dialog is stored \label{}} for each group the student is a member of. When storing and replacing the previous dialogstate, this dialogstate is transferred to the history of the usermodel (eventually after compression).
240 {\bf\SR The dialogstate has the attributes \label{}}
243 12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
244 \>begin \>\>\>\>\>\>\>\>\>timestamp of begin of session\\
245 \>provided-end\>\>\>\>\>\>\>\>\>e.g. for examinations\\
246 \>actual-end \>\>\>\>\>\>\>\>\>empty, or timestamp of end of session\\
247 \>group \>\>\>\>\>\>\>\>\>the user has started the session with\\
248 \>interactions, for each: \\
250 \>\>label of example\>\>\>\>\>\>\>\>empty if \sisac{} entered via KB\\
251 \>\>input\>\>\>\>\>\>\>\>tactic, formula, command or label in KB\\
252 \>\>response\>\>\>\>\>\>\>\>??? of which part of system ???\\
253 \>\>pattern\>\>\>\>\>\>\>\>of dialog\\
256 \>\>\>\dots TODO \dots\\
258 The use of these fields is shown by use-case UC TODO.
261 \subparagraph{The usermodel} consists of two parts: the settings of the personal preferences and the history of (condensed) dialogstates. The history is constructed from the dialogstates: before a dialogstate is being replaced at the start of a new session, its data are restructured and appended to the history.
262 {\bf\SR The usermodel has the attributes\label{}}
265 12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill
267 \>\>patterns, for each:\>\>\>\>\>\>\>\>of dialog\\
270 \>\>\>\dots TODO \dots\\
271 \>history, for each session:\>\>\>\>\>\>\>\>\>\\
272 \>\>begin\_end\>\>\>\>\>\>\>\>2 timestamps\\
273 \>\>group\>\>\>\>\>\>\>\> the user has started the session with\\
274 \>\>kb\_touchs, for each:\>\>\>\>\>\>\>\>\\
275 \>\>\>label of KB item\\
277 \>\>examples, for each:\\
278 \>\>\>label of example\\
279 \>\>\>begin\_end\>\>\>\>\>\>\>2 timestamps\\
280 \>\>\>finished\>\>\>\>\>\>\>yes/no\\
281 \>\>\>performance\>\>\>\>\>\>\>from example.evaluation.TODO and\\
282 \>\>\>\>\>\>\>\>\>\>from dialog.interactions\\
284 The use of these fields is shown by use-case UC TODO.
287 \section{The mathematics engine}
288 Here only these requirements are recorded which have been newly raised when specifying the interfaces to the ME.
290 {\bf\SR The structure of a calculation is given by ??? for each formula\label{}}