XASM Components

The declaration of sub-asms and external functions that refer to other asms in the specification requires that the existence and functionality of these asms is known at specification time. This is comparable to a static module concept and is useful for defining sub-parts of one specific formalization. In order to be ``component-based'' like announced above, the module concept must be enriched with some other features allowing a more flexible and comfortable definition of reusable units.

For example, consider the following asm that may be used in the context of a programming language semantics specification. It checks, whether a given variable is defined in the current block, or in one of the parent blocks. The information whether a variable is defined in a certain block is stored in the ASM function DeclTable; the block structure is stored in the function ParentBlock mapping blocks to its corresponding parent blocks:

Note, that these function works correctly without recursively calling itself; it iterates until no update changes the internal state of the asm.

The ``accesses'' construct is used to specify the functions the asm expects from its parent asm. Now, with this additional meta information, the asm can be regarded as a component, because its provides information necessary to be processed as stand-alone unit. The asm can be separately compiled and put into the XASM component library; other formalization can reuse it provided that they declare the required functions.

Besides the ``accesses'' construct, which allows to read the locations of the corresponding functions provided by the parent asm, the XASM ``updates'' construct marks the corresponding function as readable and writable for the sub-asm or ASM function. In the previous example, the mode function must be marked as ``updated'' the two sub-asms, because it is updated in the body of each of them:

 

Like the accessed functions, the updated functions must be declared in the parent asm. In order to avoid repetitions in the source code, the notation `` $\USEDAS \keyword{subasm} \IN A$'' can be used as an abbreviation of accessing all functions and universes declared in A except those that are explicitly marked as ``updated'' by the sub-asm (analogously for asms that are used as functions).

Besides functions, sub-asms can also be contained in the ``accesses''-list of an asm-component. The accessed sub-asms are used in the rule section of the asm as if they have been declared locally.