| \documentclass[a4paper]{article} |
| \usepackage{zed-cm} |
| \usepackage{graphicx} |
| %\markboth{Draft}{Draft} |
| \pagestyle{myheadings} |
| \begin{document} |
| \parskip 6 pt |
| \parindent 0 pt |
| |
| \title{A Formal Model of the SpringSource Application Platform (v0.2)} |
| \author{Glyn Normington} |
| \maketitle |
| % The following three commands ensure the title page is stamped as |
| % confidential without a page number. Page numbering is started at the |
| % table of contents. |
| \thispagestyle{myheadings} |
| \pagenumbering{roman} |
| \setcounter{page}{0} |
| |
| %============================================================================= |
| The aim is to model the basic architecture of the SpringSource Application Platform. |
| |
| \clearpage |
| \pagenumbering{roman} |
| \tableofcontents |
| |
| % Type checking hacks |
| \newcommand{\true}{true} |
| \newcommand{\false}{false} |
| \renewcommand{\empty}{\emptyset} |
| \newcommand{\ModuleDefZero}{ModuleDef_0} |
| \newcommand{\ModuleDefOne}{ModuleDef_1} |
| \newcommand{\ModuleDefTwo}{ModuleDef_2} |
| \newcommand{\ModuleDefThree}{ModuleDef_3} |
| \newcommand{\ModuleDefFour}{ModuleDef_4} |
| |
| %============================================================================= |
| %\clearpage |
| %\pagenumbering{arabic} |
| %\section{Introduction} |
| %\label{cha:intro} |
| % |
| %To do: |
| %\begin{itemize} |
| %\item |
| %\end{itemize} |
| % |
| %============================================================================= |
| \clearpage |
| \pagenumbering{arabic} |
| \section{Standard OSGi} |
| \label{cha:standardosgi} |
| |
| Bundles have symbolic names (which are strings, but we ignore that here) and versions. |
| \begin{zed} |
| [SymbolicName, Version] |
| \end{zed} |
| |
| A bundle definition defines the bundle's name and version as well as other things we will not model here. |
| \begin{schema}{BundleDef} |
| name : SymbolicName \\ |
| version : Version \\ |
| \end{schema} |
| |
| A bundle can be in one of several states. |
| \begin{zed} |
| BundleState ::= bundleInstalled | bundleResolved | bundleStarting | \\ |
| \t1 bundleActive | bundleUnknown | bundleStopping | bundleUninstalled |
| \end{zed} |
| \textit{Note : we are modelling a bundle instance rather than |
| a bundle definition, so we may not need the uninstalled state.} |
| |
| We'll need to talk about class loaders but only in terms of them providing a name space for classes. |
| \begin{zed} |
| [ClassName, Class] |
| \end{zed} |
| |
| We currently ignore the distinction between initiating and defining class loaders and model a class |
| loader as a one-one map of class names to classes. |
| \begin{schema}{ClassLoader} |
| cl : ClassName \pinj Class \\ |
| \end{schema} |
| |
| Each class instance uniquely determines its defining class loader. |
| \begin{axdef} |
| getClassLoader : Class \pfun ClassLoader \\ |
| \where |
| \forall c : \dom getClassLoader @ \\ |
| \t1 c \in \ran (getClassLoader~c).cl \\ |
| \end{axdef} |
| |
| A bundle has a name and a state. |
| \begin{schema}{Bundle} |
| name : SymbolicName \\ |
| version : Version \\ |
| state : BundleState \\ |
| \end{schema} |
| |
| The standard OSGi framework uniquely identifies each installed bundle by name and version. |
| The OSGi framework also loads the classes of each bundle using a separate class loader. |
| Bundles which have reached the starting state have a class loader whereas those which are |
| installed or resolved will only have a class loader if they have reached the starting state in |
| the past. |
| \begin{schema}{StandardOSGi} |
| bundles : SymbolicName \cross Version \pinj Bundle \\ |
| cl : Bundle \pinj ClassLoader \\ |
| \where |
| \forall n : SymbolicName; v : Version; b : Bundle | \\ |
| \t1 (n, v) \mapsto b \in bundles @ \\ |
| \t2 n = b.name \land v = b.version \\ |
| \forall b : \ran bundles | \\ |
| \t1 b.state \notin \{ bundleInstalled, bundleResolved \} @ \\ |
| \t2 b \in \dom cl \\ |
| \end{schema} |
| |
| A bundle may be installed in the OSGi framework by providing its bundle definition. |
| We allow for the installation of a bundle to install other bundles (from a repository |
| as we will see later). |
| \begin{schema}{InstallBundleOk\_so} |
| \Delta StandardOSGi \\ |
| bd? : BundleDef \\ |
| \where |
| (bd?.name, bd?.version) \notin \dom bundles \\ |
| \exists Bundle' @ \\ |
| \t1 name' = bd?.name \land version' = bd?.version \land \\ |
| \t1 state' = bundleInstalled \land \\ |
| \t1 \{ (name', version') \mapsto \theta Bundle' \} \cup bundles \subseteq bundles' \\ |
| \end{schema} |
| |
| %============================================================================= |
| \clearpage |
| \section{Extended OSGi} |
| \label{cha:extendedosgi} |
| |
| The SpringSource Application Platform extends standard OSGi by adding a number of concepts |
| including the concept of a \textit{library}. |
| |
| A library has a symbolic name, a version, and a list of bundles. Each bundle |
| in the list has a unique symbolic name. |
| \begin{schema}{Library} |
| name : SymbolicName \\ |
| version : Version \\ |
| bundles : \seq Bundle \\ |
| \where |
| \forall i, j : \dom bundles @ \\ |
| \t1 (bundles~i).name = (bundles~j).name \implies i = j \\ |
| \end{schema} |
| \textit{Note: check this constraint is enforced by the Platform.} |
| |
| The extended OSGi framework adds a collection of libraries to the standard framework. |
| Each library is uniquely identified by name and version and its bundles are present in |
| the framework. |
| \begin{schema}{ExtendedOSGi} |
| StandardOSGi \\ |
| libraries : SymbolicName \cross Version \pinj Library \\ |
| \where |
| \forall n : SymbolicName; v : Version; l : Library | \\ |
| \t1 (n, v) \mapsto l \in libraries @ \\ |
| \t2 n = l.name \land v = l.version \\ |
| \forall l : \ran libraries @ \\ |
| \t1 \ran l.bundles \subseteq \ran bundles \\ |
| \end{schema} |
| |
| %============================================================================= |
| \clearpage |
| \section{Subsystems} |
| \label{cha:subsystems} |
| |
| Subsystem names are strings, but we ignore that here. |
| \begin{zed} |
| [SubsystemName] |
| \end{zed} |
| |
| A subsystem can be in one of several states. |
| \begin{zed} |
| SubsystemState ::= subsystemInstalling | subsystemInstalled | \\ |
| \t1 subsystemStarting | subsystemStarted | \\ |
| \t1 subsystemUnknown | subsystemStopping | \\ |
| \t1 subsystemStopped | subsystemUninstalling |
| \end{zed} |
| |
| The Platform is composed of \textit{subsystems} each of which has a name, a status, and a |
| set of bundles. |
| \begin{schema}{Subsystem} |
| name : SubsystemName \\ |
| state : SubsystemState \\ |
| bundles : \power Bundle \\ |
| \end{schema} |
| \textit{Note: there relationship between the state of a subsystem and the states of |
| its bundles is not modelled here. It is not an invariant except in steady states.} |
| |
| %============================================================================= |
| \clearpage |
| \section{Subsystem Registry} |
| \label{cha:subsystemRegistry} |
| |
| The subsystem registry maintains a collection of subsystems indexed by name and navigational information |
| to determine the bundle for a given class loader and the subsystem for a given bundle. |
| \begin{schema}{SubsystemRegistry} |
| ExtendedOSGi \\ |
| ss : SubsystemName \pinj Subsystem \\ |
| b : ClassLoader \pinj Bundle \\ |
| bs : Bundle \pfun Subsystem \\ |
| \where |
| b = cl\inv \\ |
| \forall n : \dom ss @ (ss~n).name = n \\ |
| \ran b \subseteq \dom bs \\ |
| \ran bs \subseteq \ran ss \\ |
| \forall s : \ran ss | s.state \neq subsystemInstalling @ \\ |
| \t1 s.bundles \subseteq bs \inv \limg \{ s \} \rimg \\ |
| \end{schema} |
| |
| \begin{schema}{getSubsystemByClassOk} |
| \Xi SubsystemRegistry \\ |
| c? : Class \\ |
| s! : Subsystem \\ |
| \where |
| \exists cl : ClassLoader | cl = getClassLoader~c? @ \\ |
| \t1 cl \in \dom b \land \\ |
| \t1 s! = bs(b~cl) \\ |
| \end{schema} |
| |
| %============================================================================= |
| \clearpage |
| \section{Repository} |
| \label{cha:repository} |
| |
| A repository holds bundle and library definitions. |
| |
| A library definition defines the library's name and version and a specification of |
| a collection of bundles. Each bundle in the specification has a name and a version |
| range (modelled here as a set of versions). |
| \begin{schema}{LibraryDef} |
| name : SymbolicName \\ |
| version : Version \\ |
| bundleSpecs : SymbolicName \pinj \power Version |
| \end{schema} |
| |
| The repository uniquely identifies each bundle and library by name and version. |
| \begin{schema}{Repository} |
| bundleDefs : SymbolicName \cross Version \pinj BundleDef \\ |
| libraryDefs : SymbolicName \cross Version \pinj LibraryDef \\ |
| \where |
| \forall n : SymbolicName; v : Version; bd : BundleDef | \\ |
| \t1 (n, v) \mapsto bd \in bundleDefs @ \\ |
| \t2 n = bd.name \land v = bd.version \\ |
| \forall n : SymbolicName; v : Version; ld : LibraryDef | \\ |
| \t1 (n, v) \mapsto ld \in libraryDefs @ \\ |
| \t2 n = ld.name \land v = ld.version \\ |
| \end{schema} |
| |
| The internal representation of a repository may be quite different from the |
| model presented here. The aim here is to provide a specification that defines |
| how a repository behaves rather than a detailed description of a particular |
| repository implementation. |
| |
| The repository provides an operation for adding a bundle. |
| \begin{schema}{AddBundleOk} |
| \Delta Repository \\ |
| bd? : BundleDef \\ |
| \where |
| (bd?.name, bd?.version) \notin \dom bundleDefs \\ |
| bundleDefs = bundleDefs \cup \{ (bd?.name, bd?.version) \mapsto bd? \} \\ |
| \end{schema} |
| |
| \textit{The implementation allows any bundle definition to be added to the |
| repository, even if it is already present.} |
| |
| The repository also provides an operation for adding a library. |
| \begin{schema}{AddLibraryOk} |
| \Delta Repository \\ |
| ld? : LibraryDef \\ |
| \where |
| (ld?.name, ld?.version) \notin \dom libraryDefs \\ |
| libraryDefs = libraryDefs \cup \{ (ld?.name, ld?.version) \mapsto ld? \} \\ |
| \end{schema} |
| |
| %============================================================================= |
| \clearpage |
| \section{Installation} |
| \label{cha:installation} |
| |
| Bundles are installed in OSGi and then started in order to initialise the |
| Platform and to deploy applications on to the Platform. |
| |
| Installation takes some bundles and attempts to satisfy their dependencies by |
| implicitly installing other bundles from the repository. Installation automatically starts |
| bundles implicitly installed from the repository, but does not start the |
| bundles that were input to installation. |
| \begin{schema}{InstallBundle} |
| \Xi Repository \\ |
| \Delta ExtendedOSGi \\ |
| InstallBundleOk\_so \\ |
| \where |
| \exists i : SymbolicName \cross Version \pinj BundleDef @ \\ |
| \t1 i \subseteq bundleDefs \land \\ |
| \t1 \dom bundles' = \dom bundles \cup \{ (bd?.name, bd?.version)\} \cup \dom i \\ |
| \end{schema} |
| \textit{Note: the above schema does not model the states of the implicitly installed |
| bundles. Each such bundle is installed from the corresponding bundle definition |
| in the repository and is started after being installed.} |
| |
| %============================================================================= |
| \clearpage |
| \section{Deployment} |
| \label{cha:deployment} |
| |
| Quite separately from the installation of bundles during deployment, we need to model the way |
| application deployment is exposed to the user. |
| |
| Users deal with deployable artefacts such as Platform archive files (PARs), web archive files (WARs), and single OSGi bundles (JARs). We abstract away from the differences and model a deployable |
| artefact as having just a \textit{deployment identity} consisting of a symbolic name and a version. |
| \begin{schema}{DeploymentIdentity} |
| name : SymbolicName \\ |
| version : Version \\ |
| \end{schema} |
| |
| We don't bother modelling the contents of a deployment artefact other than its deployment identifier. |
| of deployable artefacts. |
| \begin{schema}{DeployableArtefact} |
| DeploymentIdentity \\ |
| \end{schema} |
| |
| A deployable artefact may be deployed either by calling a Platform API passing the location of |
| the artefact in the file system or by copying the artefact into the Platform's hot deployment |
| directory. |
| \begin{zed} |
| [Location] |
| \end{zed} |
| |
| \begin{zed} |
| Boolean ::= yes | no |
| \end{zed} |
| |
| \begin{schema}{FileSystem} |
| fs: Location \pfun DeployableArtefact \\ |
| \end{schema} |
| |
| Artefacts deployed in the Platform are identified by name and version. Artefacts which were |
| hot deployed are stored in a portion of the file system and each such artefact has a unique |
| location within that portion of the file system. Some deployed artefacts are recoverable |
| including all those stored in the deployer's portion of the file system. |
| \begin{schema}{Deployed} |
| dep : DeploymentIdentity \pinj DeployableArtefact \\ |
| rec : \power DeployableArtefact \\ |
| FileSystem_0 \\ |
| \where |
| \forall DeploymentIdentity; da : DeployableArtefact | \\ |
| \t1 \theta DeploymentIdentity \mapsto da \in dep @ \\ |
| \t2 name = da.name \land version = da.version \\ |
| \ran fs_0 \subseteq \ran dep \\ |
| fs_0 \in Location \pinj DeployableArtefact \\ |
| rec \subseteq \ran dep \\ |
| \ran fs_0 \subseteq rec \\ |
| \end{schema} |
| |
| Deploying from a location stores the deployable artefact but does not remember the location. |
| \begin{schema}{DeployLocationOk} |
| \Xi FileSystem \\ |
| \Delta Deployed \\ |
| loc? : Location \\ |
| recoverable? : Boolean \\ |
| \where |
| \dom fs_0 \cap \dom fs = \empty \\ |
| loc? \in \dom fs \\ |
| fs_0' = fs_0 \\ |
| \exists d : DeployableArtefact; DeploymentIdentity | \\ |
| \t1 d = fs~loc? \land d.name = name \land d.version = version @ \\ |
| \t1 \theta DeploymentIdentity \notin \dom dep \land \\ |
| \t1 dep' = dep \cup \{\theta DeploymentIdentity \mapsto d\} \land \\ |
| \t1 recoverable? = yes \implies rec' = rec \cup \{d\} \\ |
| recoverable? = no \implies rec' = rec \\ |
| \end{schema} |
| |
| Hot deploying a deployable artefact stores the artefact and gives it a location in the deployer's |
| portion of the file system. |
| \begin{schema}{HotDeployOk} |
| \Xi FileSystem \\ |
| \Delta Deployed \\ |
| da? : DeployableArtefact \\ |
| \where |
| \exists DeploymentIdentity | name = da?.name \land version = da?.version @ \\ |
| \t1 \theta DeploymentIdentity \notin \dom dep \land \\ |
| \t1 dep' = dep \cup \{\theta DeploymentIdentity \mapsto da?\} \\ |
| \exists l' : Location | l' \notin \dom fs \cup \dom fs_0 @ \\ |
| \t1 fs_0' = fs_0 \cup \{l' \mapsto da?\} \\ |
| rec' = rec \cup \{da?\} \\ |
| \end{schema} |
| |
| A artefact that has already been deployed can be undeployed in a number of ways. The most |
| general way is to pass in deployment identity (equivalent to the name and version). |
| \begin{schema}{UndeployNameVersionOk} |
| \Delta Deployed \\ |
| di? : DeploymentIdentity \\ |
| \where |
| di? \in \dom dep \\ |
| dep' = \{di?\} \ndres dep \\ |
| fs_0' = fs_0 \nrres \{dep~di?\} \\ |
| rec' = rec \setminus \{dep~di?\} \\ |
| \end{schema} |
| |
| The other way to undeploy an artefact is to delete an artefact that was hot deployed which we |
| model as passing in the location of the hot deployed artefact. |
| \begin{schema}{HotUndeployOk} |
| \Delta Deployed \\ |
| loc? : Location \\ |
| \where |
| loc? \in \dom fs_0 \\ |
| fs_0' = \{loc?\} \ndres fs_0 \\ |
| dep' = dep \nrres \{fs_0~loc?\} \\ |
| rec' = rec \setminus \{fs_0~loc?\} \\ |
| \end{schema} |
| |
| Recovery deletes non-recoverable artefacts. |
| \begin{schema}{Recover} |
| \Delta Deployed \\ |
| \where |
| dep' = dep \rres rec \\ |
| rec' = rec \\ |
| fs_0' = fs_0 \\ |
| \end{schema} |
| |
| |
| %============================================================================= |
| \newpage |
| \section{Z Notation} |
| \label{cha:znot} |
| |
| \makeatletter % the following code is taken from Mike Spivey's zed.tex |
| |
| \def\symtab{\setbox0=\vbox\bgroup \def\\{\cr} |
| \halign\bgroup\strut$##$\hfil&\quad##\hfil\cr} |
| \def\endsymtab{\crcr\egroup\egroup |
| \dimen0=\ht0 \divide\dimen0 by2 \advance\dimen0 by\ht\strutbox |
| \splittopskip=\ht\strutbox \vbadness=10000 |
| \predisplaypenalty=0 |
| $$\halign{##\cr\hbox to\linewidth{% |
| \valign{##\vfil\cr |
| \setbox1=\vsplit0 to\dimen0 \unvbox1\cr |
| \noalign{\hfil}\unvbox0\cr |
| \noalign{\hfil}}}\cr |
| \noalign{\prevdepth=\dp\strutbox}}$$ |
| \global\@ignoretrue} |
| |
| \makeatother |
| |
| Numbers: |
| \begin{symtab} |
| \nat & \verb/Natural numbers/ \{\verb/0,1,.../\} \\ |
| % \num & \verb/Integers (...,-1,0,1,...)/ \\ |
| % \nat_1 & \verb/Positive natural numbers/ \\ |
| % \upto & \verb/integral range/ \\ |
| % + & \verb/Addition/\quad\hfill 3 \\ |
| % - & \verb/Subtraction/\quad\hfill 3 \\ |
| % * & \verb/Multiply/\quad\hfill 4 \\ |
| % \div & \verb/Remainder/\quad\hfill 4 \\ |
| % \mod & \verb/Modulus/\quad\hfill 4 \\ |
| % < & \verb/Less than/ \\ |
| % > & \verb/Greater than/ \\ |
| % \leq & \verb/Less than or equal/ \\ |
| % \geq & \verb/Greater than or equal/ \\ |
| % \neq & \verb/Inequality/ \\ |
| \end{symtab} |
| Propositional logic and the schema calculus: |
| \begin{symtab} |
| % \lnot & \verb/Not/ \\ |
| \ldots\land\ldots & \verb/And/ \\ |
| \ldots\lor\ldots & \verb/Or/ \\ |
| \ldots\implies\ldots & \verb/Implies/ \\ |
| % \iff & \verb/If and only if/ \\ |
| \forall..\mid..\spot.. & \verb/For all/ \\ |
| \exists..\mid..\spot.. & \verb/There exists/ \\ |
| % \exists_1..\mid..\spot.. & \verb/There exists unique/ \\ |
| \ldots\hide\ldots & \verb/Hiding/ \\ |
| % \project & \verb/\project/ \\ |
| % \pre & \verb/\pre/ \\ |
| % \semi & \verb/\semi/ |
| \ldots\defs\ldots & \verb/Schema definition/ \\ |
| \ldots==\ldots & \verb/Abbreviation/ \\ |
| \ldots::=\ldots\mid\ldots & \verb/Free type definition/ \\ |
| \ldata\ldots\rdata & \verb/Free type injection/ \\ |
| [\ldots] & \verb/Given sets/ \\ |
| ',?,!,_0\ldots_9 & \verb/Schema decorations/ \\ |
| \ldots\shows\ldots & \verb/theorem/ \\ |
| \theta\ldots & \verb/Binding formation/ \\ |
| \lambda\ldots & \verb/Function definition/ \\ |
| \mu\ldots & \verb/Mu-expression/ \\ |
| \Delta\ldots & \verb/State change/ \\ |
| \Xi\ldots & \verb/Invariant state change/ \\ |
| \end{symtab} |
| Sets and sequences: |
| %and bags: |
| \begin{symtab} |
| \{\ldots\} & \verb/Set/ \\ |
| \{..\mid..\spot..\} & \verb/Set comprehension/ \\ |
| \power\ldots & \verb/Set of subsets of/ \\ |
| % \power_1 & \verb/Non-empty subsets of/ \\ |
| % \finset & \verb/Finite sets/ \\ |
| % \finset_1 & \verb/Non-empty finite sets/ \\ |
| \emptyset & \verb/Empty set/ \\ |
| \ldots\cross\ldots & \verb/Cartesian product/ \\ |
| \ldots\in\ldots & \verb/Set membership/ \\ |
| \ldots\notin\ldots & \verb/Set non-membership/ \\ |
| \ldots\cup\ldots & \verb/Union/ \\ |
| \ldots\cap\ldots & \verb/Intersection/ \\ |
| \ldots\setminus\ldots & \verb/Set difference/ \\ |
| \bigcup\ldots & \verb/Distributed union/ \\ |
| % \bigcap & \verb/Distributed intersection/ \\ |
| \#\ldots & \verb/Cardinality/ \\ |
| % \dcat & \verb/Distributed sequence concatenation/ |
| \ldots\subseteq\ldots & \verb/Subset/ \\ |
| \ldots\subset\ldots & \verb/Proper subset/ \\ |
| \ldots\partition\ldots & \verb/Set partition/ \\ |
| \seq & \verb/Sequences/ \\ |
| % \seq_1 & \verb/Non-empty sequences/ \\ |
| % \iseq & \verb/Injective sequences/ \\ |
| \langle\ldots\rangle & \verb/Sequence/ \\ |
| % \cat & \verb/Sequence concatenation/ \\ |
| \disjoint\ldots & \verb/Disjoint sequence of sets/ \\ |
| % \bag & \verb/Bags/ \\ |
| % \lbag\ldots\rbag & \verb/Bag/ \\ |
| % \inbag & \verb/Bag membership/ \\ |
| \end{symtab} |
| %Here are the infix function symbols. Each symbol is |
| %shown with its priority: |
| %\begin{symtab} |
| % \uplus & \verb/\uplus/ \\ |
| % \filter & \verb/Schema projection/ \\ |
| % \uminus & \verb/\uminus/ |
| %\end{symtab} |
| Functions and relations: |
| \begin{symtab} |
| \ldots\rel\ldots & \verb/Relation/ \\ |
| \ldots\pfun\ldots & \verb/Partial function/ \\ |
| \ldots\fun\ldots & \verb/Total function/ \\ |
| \ldots\pinj\ldots & \verb/Partial injection/ \\ |
| \ldots\inj\ldots & \verb/Injection/ \\ |
| % \psurj & \verb/Partial surjection/ \\ |
| % \surj & \verb/Surjection/ \\ |
| % \bij & \verb/Bijection/ \\ |
| % \ffun & \verb/Finite partial function/ \\ |
| % \finj & \verb/Finite partial injection/ \\ |
| \dom\ldots & \verb/Domain/ \\ |
| \ran\ldots & \verb/Range/ \\ |
| \ldots\mapsto\ldots & \verb/maplet/ \\ |
| \ldots\inv & \verb/Relational inverse/ \\ |
| % \ldots\plus & \verb/Transitive closure/ \\ |
| \ldots\star & \verb/Reflexive-transitive closure/ \\ |
| % \ldots\bsup n \esup & \verb/Relational iteration/ \\ |
| \ldots\limg\ldots\rimg & \verb/Relational image/ \\ |
| % \comp & \verb/Forward relational composition/ \\ |
| % \circ & \verb/Relational composition/ \\ |
| \ldots\oplus\ldots & \verb/Functional overriding/ \\ |
| \ldots\dres\ldots & \verb/Domain restriction/ \\ |
| % \ldots\rres\ldots & \verb/Range restriction/ \\ |
| \ldots\ndres\ldots & \verb/Domain subtraction/ \\ |
| % \ldots\nrres\ldots & \verb/Range subtraction/ \\ |
| % \id & \verb/Identity relation/ \\ |
| \end{symtab} |
| Axiomatic descriptions: |
| %%unchecked |
| \begin{axdef} |
| Declarations |
| \where |
| Predicates |
| \end{axdef} |
| Schema definitions: |
| %%unchecked |
| \begin{schema}{SchemaName} |
| Declaration |
| \where |
| Predicates |
| \end{schema} |
| \end{document} |