Abstract This document describes AsmL, a specification language based on abstract state machines. Foundations of Software Engineering Microsoft Research (c) Microsoft Corporation. All rights reserved. Contents 1 Introduction 6
Download 0.93 Mb.
|
- Navigate this page:
- 1.63Literate programming environment
- 10.NET Extensions
- 1.64Modifiers
1.62LinkageAsmL does not specify how it interacts with entities provided by the external environment. The representation of values by the language implementation is abstract. The mechanism by which AsmL invokes external, foreign routines that are introduced by import directives is not part of AsmL. In particular, if external routines must be invoked in a particular order, the steps of an abstract state machine must explicitly give this order. (By design, the order of evaluation of expressions within a step is not specified.) Except for the convention of the name Main to denote the program’s entry point, the way in which AsmL programs may be invoked by the outside environment is not part of AsmL. For example, AsmL does not have the concept of a thread of execution, since all computation within a step of an abstract state machine proceeds in parallel. An AsmL implementation is free to interact with the external operating environment in any way that preserves the semantics of the language, for example, by using as many processes and threads as it desires. Different implementations might make very different choices in this area. Thus, the language definition does not specify the mechanism for synchronizing AsmL objects with those provided by an external runtime environment. Nonetheless, Microsoft's implementation of AsmL for Windows provides extensive integration with .NET. (This integration provides for synchronization between AsmL objects and the external environment, but this is not part of AsmL.) As a result, AsmL models may be invoked from test harnesses written in any .NET-compliant language such as Visual Basic.NET and Visual C#. The .NET integration is described in separate documentation. It may come as a surprise that an implementation of a language focused on rigorous semantic modeling devotes so much energy on integration with an external operating environment. Our experience so far is that sophisticated integration with external operating environments is an essential part of making rigorous approaches relevant to software specification and testing in the commercial environment. As an example of this point, the .NET integration provided by Microsoft's AsmL compiler has been used by test harnesses that check whether an implementation (written in a standard commercial programming language) agrees at runtime with its (mathematically precise) executable specification written in AsmL.
In Microsoft, virtually all specification documents used for internal development projects are encoded as binary files in Microsoft Word (".doc") format. Microsoft's AsmL toolset is capable of processing AsmL source directly from Word files (using a special AsmL "style" in the word processor). The result of this processing step is a text file structured as XML markup that conforms to the "AsmL.dtd" schema. This schema allows AsmL source to be interleaved with marked-up text and links to graphics that document the design. The benefit of XML mark-up is that it has a variety of processing options in the documentation work flow, for example, as the basis of code review templates, test plans, reference material for customer support personnel and even as part of the product's external documentation. Putting AsmL-based specifications at the center of it documentation process maximizes the benefit a development team will receive from its investment in precise, testable specifications. Modifiers may be added to type declarations, members, parameters of methods and local variables. The modifiers virtual and override are used to provide methods that may be specialized by subtypes. The keyword virtual indicates that a default implementation is provided; however, a subtype may override this default. The keyword override precedes a method that replaces the default given in s supertype. (The corresponding supertype method must be virtual or abstract.) Override must be used whenever a method replacement occurs. If neither "virtual" nor "abstract" is specified in a method's declaration in the base type, then this method may not be specialized in a derived type. The extensibility modifiers (abstract and sealed) may be added to a type or member declaration to indicate whether additional definitions may (or in the case of abstract, must) be provided by subtypes. A sealed method (or any method of a sealed datatype) may not be extended. The modifier primitive may be applied to methods, method parameters and local variables. If provided, it indicates that AsmL update semantics do not apply. Instead, updates to primitive variables take effect with each update statement. AsmL's parameter modifiers allow for call-by-reference and output parameters. The modifiers for access (public, private, protected and internal) have the same meaning as other CLS-compliant languages. The modifier may limit the accessibility of a type's members. If unspecified, the type's visibility is internal. A member is accessible if it may be referred to by using a simple name, a qualified name or the dot (".") operator. Thus, if a member is not accessible in a given context, then there is no way to refer to it. The members of types declared as public are accessible in every scope. The members of types declared as private are accessible only within the lexical scope of the type's declaration. The members of types declared as protected are accessible only within the scope that contains the type declaration. The members of types declared as internal are accessible only within the current compilation unit. Private members are only visible in the current scope. They are present but not visible in subtypes. Download 0.93 Mb. Share with your friends:
|