Title
VLib: Infinite Virtual Libraries for LOTOS
Abstract
This paper introduces VLib, an extension to LOTOS that eases the specification of data types. It allows the definition and use of virtual libraries containing conceptually an infinite number of data types. The extraction of a working finite subset for a particular application is also considered. After a general introduction to LOTOS data specification issues, the extension is explained and formally defined. A prototype tool implementing the extraction operation is described, and a specification discipline is proposed that benefits from the provided gain of functionality. The formal specification language LOTOS was standardized by ISO (ISO89) and has been applied to numerous developments, both in the applicative and theoretical domains. LOTOS combines two clearly distinguished concepts: process algebras for describing behaviours and algebraic specifications for defining data structures. Both are oriented towards a high abstraction level supported by a strong mathematical basis. The latter is based on the language ACT ONE (Ehrig85) and will be at the centre of the study presented here. ACT ONE is a powerful tool for reasoning about the properties of data structures. With use however it appears that it is not so well fitted for its practical use in the specification of real systems: whereas its considerable expression power is generally under-used, the very basic nature of its building elements (sorts, operations and equations) and the rigidity of its model lead to lengthy specifications with lots of repetitive, technical details that clutter the data part of the specification. This has been universally recognized as one of the major obstacles against a widespread use of LOTOS by distributed systems designers, and will surely be a major concern for a future revision of LOTOS by ISO (Brinksma92). In the present situation however, the only recognized language is the one defined in the standard. Moreover all supporting software tools are based on that standard: since one can hardly afford any specification effort without such tools, usage of standard ACT ONE remains the rule. We propose in this paper a slight extension of the concept of library that is available in standard LOTOS. We introduce virtual libraries containing conceptually an infinite number of data type definitions. This allows us to cover collections of common types such as tuples, which could not appear in the standard library because they are infinite. To define virtual libraries, generic macro constructions are added to the language. According to the types
Year
Venue
Keywords
1993
PSTV
language constructs and features,programming languages,infinite virtual libraries,processors,distributed system,data structure,expressive power,process algebra,programming language,data type
Field
DocType
Volume
Specification language,Programming language specification,Programming language,Computer science,Language Of Temporal Ordering Specification
Conference
16
ISSN
ISBN
Citations 
0926-549X
0-444-81648-8
1
PageRank 
References 
Authors
0.88
7
1
Name
Order
Citations
PageRank
Charles Pecheur128428.50