%nicht vergessen: auch srd.tex ($Revision $) \"andern !

\part{Software Requirements Document}

This Software Requirements Document is structured along the modules

abstracted from the functionality defined in the User Requirements

Document. The User Requirements Document, however, is structured along

the different kinds of users envisaged. In order to establish

comfortable tracing, the $m:n$ relation between user requirements and

software requirements will be accurrately recorded in a double-linked

way.

\chapter{General requirements}

%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.

\subparagraph{Delopment environment,} standards and components, documentation and revision control are described in appendix \ref{AP:environment}.

\subparagraph{Decisions for underlying systems} have been done already.

As this requirements document shows, \sisac{} is a large system: thus it cannot be done from scratch, rather is has to use as much as components already available. The theorem prover Isabelle provides for both, a comprehensive frontend for interactive deduction (i.e. for definitions, axioms and proving theorems), and a hughe mathematics knowledge base. Both are under rapid development, which \sisac{} shall take advantage of. The kernel of Isabelle, however is relatively stable already, and thus the interfaces to \sisac s math engine (ME) are sufficiently stable.

{\bf\SR The deductive part is left to Isabelle. \label{deduct-isa}}

{\bf\SR \sisac s math engine closely cooperates with Isabelle \label{me-isa}\\}

Thus the math engine is already implemented in the same program language as Isabelle, SML.

%dropped: visitor canNOT calculate !

%

%\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).

%{\bf\SR Browsers are called by a 'master-browser' {\em and} by the worksheet. \label{}} ??? %WN2.12.02 ...... ausbessern !!!!

\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

 \sisac-components belonging to these two language environments. 

{\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.

{\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.

\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.

{\bf\SR On the client-side a Java virtual machine version .... \label{}} must reside on the local computer of the learners and authors.

{\bf\SR On the server there is a Linux or Unix \label{}} operating system, Linux version ..., Unix ...

\chapter{The worksheet}

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. 

\subparagraph{A calculation mirrors the structure of the prooftree.}

{\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.

{\bf\SR Export a calculation to a standard format \label{}} preferably XML plus MathML. 

%{\bf\SR \label{}}

\chapter{The browser generators}

 \sisac's mathematics knowledge (on (1)theories (2)problems (3)methods)

 is held in SML datastructures. Here we describe all requirements

 concerning the generation of the browsers written in Java, whereas

 the generation of the math knowledge itself is described in the

 'interfaces for authors of math knowledge'.

The browser generators provide the contents for the browsers. This

means that a browser querys its respective browser generator about

subnodes etc. whereas the further description is held outside the

SML-engine. To maintain this connection, unique identifyer are needed.

{\bf\SR browser-generators use locally unique identifyers \label{}} (locally unique within SML) for their informations (for each node of their structure).

\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.)

{\bf\SR The hiearchy  displayed in a frame \label{}} in order to have it visible all the time.

{\bf\SR The hierarchy has arbitrary levels. \label{}} For the headlines for each level see SR \dots SR \ref{expl-headlines}.

{\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.

\section{The theory browser generator}

The generation of the theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.

{\bf\SR The theory browser generator is given by Isabelle. \label{gen-isa}} 

\section{The problem and method browser generators}

.

\section{The example browser generator}

This authoring component comprises all tools necessary to generate the content displayed by the example browser. 

{\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}). 

{\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.

\chapter{The knowledge browsers}

\label{kbrowser}

%W.N.: dieser Abschnitt ist f''ur A.G. + W.N.

All browsers (Example-Browser and Knowledge-Browsers) present their

output in a similar way. Textual descriptions have to be combined with

images, formulas, formalisations, problems, \dots and links to further

informations(UR\ref{URinterlink}). The structure of this informations

has to be taken from the respective browser-generators. All kinds of

information might be interlinked among each other, but not all parts

of the information might be already present in the system when a new

item is inserted. (e.g. a example might use the keyword

\emph{is\_rooteq\_in} in its \emph{where}\/clause before the keyword

is described in the system. If the example is viewed after a

description became available, a link to the explanation should be

provided automatically.) To support this feature, the browsers need a

fast way to look up a special description.

{\bf\SR fast look up for description (includes resolve of the

identifyer and query for a description)}

\subparagraph{Groups of users} are usually 1-to-1 related to courses; members of courses get specific examples and specific advice by explanations.

{\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.

{\bf\SR There is a default group for visitors. \label{}}

{\bf\SR \label{}}

\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.

{\bf\SR Additional data and visibility are course specific. \label{}}

{\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).

\section{The theory browser}

The theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.

{\bf\SR the theory browser is given by Isabelle. \label{}} 

\section{The problem and method browsers}

%\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.

%{\bf\SR Browsers create the presentation in browser-windows dynamically. \label{}}

\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}). 

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.

{\bf\SR A problem-page consists of \label{problem-page}} the 

\begin{tabbing}

12345\=123\=123\=\kill

\>name of the problem\\

\>the fields 'given', 'where', 'find' and 'relate'\\

\>a link to the special math data\\

\>a list of subordinated methods (only displayed in the hierarchy-frame)\\

\>an arbitrary list of links to additional data

\end{tabbing}

The next lower and next higher level in the hierarchy can be found in the hierarchy-frame.

{\bf\SR A method-page consists of \label{method-page}}

\begin{tabbing}

12345\=123\=123\=\kill

\>name of the method\\

\>the script\\

\>a link to the special math data\\

\>a list of subordinated methods (only displayed in the hierarchy-frame)\\

\>an arbitrary list of links to additional data

\end{tabbing}

{\bf\SR The links to additional data \label{}} have the following attributes:

\begin{tabbing}

12345\=123\=123\=\kill

\>text on the link\\

\>the reference (to an explanation or to an example starting a worksheet)\\

\>groups\\

\>\>ID of first group\\

\>\>\>locked: list of intervals\\

\>\>\>???used by userID ---$>$ usermodel???\\

\>\>ID of second group \dots

\end{tabbing}

%{\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).

%{\bf\SR Access to explanations and examples of other courses \label{}} is possible by ... ??? (see UR \ref{other-courses}).

\section{The example browser}

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.

\subparagraph{Attributes of examples and collections} are numerous, and thus defaults help to safe space. There is only one collection, partitioned hierarchically into subcollections.

{\bf\SR Default data \label{}} are filled in bottum up: A default is filled by the first non-default parent.

{\bf\SR A subcollection has the attributes \label{coll-attr}}

\begin{tabbing}

12345\=123\=123\=123\=123\=\kill

\>headline of the collection (displayed also in the hiearchy-frame) \\

\>description of the collection\\

\>list of subcollections\\

\>OR\\

\>layout of examples belonging to this subcollection\\

\>author\\

\>copyright owner\\

\>groups of users, for each group: \\

\>\>ID of the group \\

\>\>schemas \\

\>\>\>error \\

\>\>\>fill-in \\

\>\>\> \\

\>\>dialog \\

%\>\>\>blackbox \\

\>\>\>detail \\

\>\>\>activity \\

\>\>\>stepwidt \\

\>\>\> \\

\>\>invisible: list of intervals OR duration (? TODO !)\\

\>\>locked: list of intervalsOR duration (? TODO !) \\

\>\>evaluation \\

\>\>\>TODO: difficulty, length, \dots \\

\>\>\>finished-by: \\

\>\>\>\>elements: list of mandatory examples (or groups) to be done \\

\>\>\>\>number: number of (arbitrary) examples (or groups) to be done \\

\>\>\>\>points: calculated from TODO: difficulty, length, \dots \\

\end{tabbing}

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}.

{\bf\SR An example has the attributes \label{expl-att}}

\begin{tabbing}

12345\=123\=123\=123\=123\=123\=\kill

\>label \\

\>reference ??? to the description of the example (in the layout ?)\\

\>list of formalizations and specifications \\

\>author\\

\>copyright owner\\

\>time stamp\\

\>groups of users, for each group: \\

\>\>ID of the group \\

\>\>schemas \\

\>\>\>error \\

\>\>\>fill-in \\

\>\>\> \\

\>\>dialog \\

\>\>\>blackbox \\

\>\>\>detail \\

\>\>\>activity \\

\>\>\>stepwidt \\

\>\>\> \\

\>\>invisible: list of intervals OR duration (? TODO !) \\

\>\>locked: list of intervals OR duration (? TODO !)\\

\>\>evaluation \\

\>\>\>TODO: difficulty, length, \dots \\

\>\>???done by userID ---$>$ usermodel??? 

\end{tabbing}

{\bf\SR Hitting the label of the example starts the calculation. \label{}}

\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.

{\bf\SR {\em Only} visible examples are checked for being locked.\label{}}

%{\bf\SR Authoring-/learner-mode:} the formalization and other attributes are shown/not shown, depending on the group the user belongs to.

%\subparagraph{}

%{\bf\SR \label{}}

\chapter{The dialog guide}

%{\bf\SR A learner has a dialog state within the current session. \label{}}

%{\bf\SR Each learner has a history of all sessions. \label{}}

%{\bf\SR The history holds the condensed performance in calculations. \label{}}

%{\bf\SR The history holds requests into the knowledge. \label{}\\}

%\subparagraph{}

%{\bf\SR \\}

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.

\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.

{\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).

{\bf\SR The dialogstate has the attributes \label{}}

{\small

\begin{tabbing}

12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill

\>begin       \>\>\>\>\>\>\>\>\>timestamp of begin of session\\

\>provided-end\>\>\>\>\>\>\>\>\>e.g. for examinations\\

\>actual-end  \>\>\>\>\>\>\>\>\>empty, or timestamp of end of session\\

\>group       \>\>\>\>\>\>\>\>\>the user has started the session with\\

\>interactions, for each: \\

\>\>timestamp\\

\>\>label of example\>\>\>\>\>\>\>\>empty if \sisac{} entered via KB\\

\>\>input\>\>\>\>\>\>\>\>tactic, formula, command or label in KB\\

\>\>response\>\>\>\>\>\>\>\>??? of which part of system ???\\

\>\>pattern\>\>\>\>\>\>\>\>of dialog\\

\>\>\>activity\\

\>\>\>stepwidt\\

\>\>\>\dots TODO \dots\\

\end{tabbing}}

The use of these fields is shown by use-case UC TODO.

\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.

{\bf\SR The usermodel has the attributes\label{}}

{\small

\begin{tabbing}

12345\=123\=123\=123\=123\=123\=123\=123\=12345123\=123\=\kill

\>settings\\  

\>\>patterns, for each:\>\>\>\>\>\>\>\>of dialog\\  

\>\>\>activity\\

\>\>\>stepwidt\\

\>\>\>\dots TODO \dots\\

\>history, for each session:\>\>\>\>\>\>\>\>\>\\  

\>\>begin\_end\>\>\>\>\>\>\>\>2 timestamps\\  

\>\>group\>\>\>\>\>\>\>\> the user has started the session with\\  

\>\>kb\_touchs, for each:\>\>\>\>\>\>\>\>\\  

\>\>\>label of KB item\\  

\>\>\>timestamps\\

\>\>examples, for each:\\  

\>\>\>label of example\\  

\>\>\>begin\_end\>\>\>\>\>\>\>2 timestamps\\  

\>\>\>finished\>\>\>\>\>\>\>yes/no\\

\>\>\>performance\>\>\>\>\>\>\>from example.evaluation.TODO and\\  

\>\>\>\>\>\>\>\>\>\>from dialog.interactions\\  

\end{tabbing}}

The use of these fields is shown by use-case UC TODO.

%\chapter{The mathematics engine}

%Here only these requirements are recorded which have been newly raised when specifying the interfaces to the ME.

%

%{\bf\SR The structure of a calculation is given %by ??? for each formula

%\label{}}