This document is available in various formats from the CoFI archives at ftp://ftp.brics.dk/Projects/CoFI/Bibliography/Abstracts/.Copyright ©2004 CoFI, The Common Framework Initiative for Algebraic Specification and Development.1
This bibliography lists the entries in the file cofi.bib, in the order in which they occur, showing their citation tags and abstracts. See the changes document for a list of changes.The abbreviated, annotated,and the unabbreviated bibliographies list the same references as this bibliography. The cross-referenced proceedings and books are listed separately.
Abstract: We define an extension of Casl, the standard language for algebraic specification, with a late binding mechanism. More precisely, we introduce a special kind of functions called methods, for which, differently to what happens for usual functions, overloading resolution is delayed at evaluation time and not required to be conservative. The extension consists, at the semantic level, in the definition of an institution LBInst supporting late binding which is defined on top of the standard subsorted institution of Casl and, at the linguistic level, in the enrichment of the Casl language with appropriate constructs for dealing with methods. In addition to this, we propose a further enrichment of the Casl language which is made possible by introduction of late binding, that is a mechanism for "inheriting" axioms from a supersort with the possibility of overriding them. The aim is to obtain advantages in terms of reuse of specifications similar to those obtained by inheritance in object-oriented programming languages.
Abstract: The status of the Common Framework Initiative (CoFI) and the Common Algebraic Specification Language (Casl) are briefly presented. One important outstanding point concerns the relationship between Casl and programming languages; making a proper connection is obviously central to the use of Casl specifications for software specification and development. Some of the issues involved in making this connection are discussed.
Abstract: Algebraic/logic methods have also found interesting applications to the specification, design, and implementation of concurrent systems.Due to the particularly complex nature of concurrent systems, and contrary to the case of classical (static) data structures, there are different ways of exploiting algebraic methods in concurrency.
In the literature, we can distinguish at least four kinds of approaches.
We have organized the paper around the classification above, providing significant illustrative examples for each of the classes.
- The algebraic techniques are used at the metalevel, for instance, in the definition or in the use of specification languages.
- A particular specification language (technique) for concurrent systems is complemented with the possibility of abstractly specifying the (static) data handled by the systems considered using algebraic specifications. We can qualify the approaches of this kind by the slogan "plus algebraic specifications of static data types".
- These methods use particular algebraic specifications having "dynamic sorts", which are sorts whose elements are/correspond to concurrent systems. We can qualify the approaches of this kind as "algebraic specifications of dynamic-data types", which are types of dynamic data.
- These methods allow us to specify an (abstract) data type, which is dynamically changing with time. In such approaches we have different "algebraic" models corresponding to different states of the system. We can qualify the approaches of this kind as "algebraic specifications of dynamic data-types"; here the data types are dynamic.
Abstract: We are interested in the composition of languages, in particular a data description language and a paradigm-specific language, from a pragmatic point of view. Roughly speaking our goal is the description of languages in a component-based style, focussing on the data definition component. The proposed approach is to substitute the constructs dealing with data from the "data" language for the constructs describing data that are not specific to the particular paradigm of the "paradigm-specific" language in a way that syntax, semantics as well as methodologies of the two components are preserved. We illustrate our proposal on a toy example: using the algebraic specification language Casl, as data language, and a "pre-post" condition logic à la Hoare, as the paradigm specific one. A more interesting application of our technique is fully worked out elsewhere and the first step towards an application to UML, that is an analysis of UML from the data viewpoint, following the guidelines given here, is sketched at the end.
Abstract: In the last ten years we have developed and experimented in a series of projects, including industry test cases, a method for the specification of reactive/distributed/... systems both at the requirement and at the design level. We present here in outline its main technical features, providing appropriate references for more detailed presentations of single aspects and applications.The overall main feature of the method is its logical (algebraic) character, because it extends to labelled transition systems the logical/algebraic specification method of abstract data types; moreover systems are viewed as data within first-order structures called LT-structures. Some advantages of the approach are the full integration of the specification of static data and of dynamic systems, which includes by free higher-order concurrency, and the exploitation of well-explored classical techniques in many respects, including implementation and tools.
Abstract: The Common Algebraic Specification Language (Casl) is an expressive language for the formal specification of functional requirements and modular design of software. It has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural specifications. Casl should facilitate interoperability of many existing algebraic prototyping and verification tools. This paper gives an overview of the Casl design. The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of Casl are briefly explained and illustrated the reader is referred to the Casl Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.
Abstract: For the recently developed specification language Casl, there exist two different kinds of proof support: while Hol-Casl has its strength in proofs about specifications in-the-small, Maya has been designed for management of proofs in (Casl) specifications in-the-large, within an evolutionary formal software development process involving changes of specifications. In this work, we discuss our integration of Hol-Casl and Maya into a powerful system providing tool support for Casl, which will also serve as a basis for the integration of further proof tools.
Abstract: In this paper we investigate formally the relationship between the notion of abstract datatypes in an arbitrary institution, found in algebraic specification languages like Clear, ASL and Casl; and the notion of schemata from the model-oriented specification language Z. To this end the institution S of the logic underlying Z is defined and a translation of Z-schemata to abstract datatypes over S is given. The notion of a schema is internal to the logic of Z and thus specification techniques of Z relying on the notion of a schema can only be applied in the context of Z. By translating Z-schemata to abstract datatypes these specification techniques can be transformed to specification techniques using abstract datatypes. Since the notion of abstract datatypes is institution independent, this results in a separation of these specification techniques from the specification language Z and allows them to be applied in the context of other, e.g. algebraic, specification languages.
Abstract: A state-based extension of the algebraic specification language Casl is presented. It permits the specification of the static part of a complex dynamic system by means of Casl and the dynamic part by means of the facilities described in the paper. The dynamic system is defined as possessing a number of states and a number of operations (procedures) for transforming one state into another. Each state possesses one and the same static part specified by Casl and a varying part specified by additional tools. The varying part includes dynamic sorts/functions/predicates and dependent functions/predicates. The dependent functions/predicates are specified by formulae using the names of the dynamic functions/predicates so that each time one of the last ones is updated the corresponding former ones are also updated. The updates of the dynamic entities are produced by procedures which are specified by means of preconditions, postconditions and dynamic equations.
Abstract: This part of the Casl Reference Manual defines the formal semantics of the language Casl, as informally presented in the Casl Summary (Part I). Apart from this Introduction, which is partly devoted to defining some basic notation and explaining the style of the semantics, the structure of this document is deliberately almost identical to the structure of the Casl Summary to aid cross-reference. As in the Casl Summary, Chap. 2 deals with many-sorted basic specifications, and Chap. 3 extends this by adding features for subsorted basic specifications. Chapter 4 provides structured specifications, together with specification definitions, instantiations, and views. Chapter 5 summarizes architectural and unit specifications, which, in contrast to structured specifications, prescribe the separate development of composable, reusable implementation units. Finally, Chap. 6 considers specification libraries.The first section of each chapter defines the semantic concepts underlying the kind of specification concerned, with the remaining sections presenting the abstract syntax of the associated Casl language constructs and defining their semantics. The abstract syntax is identical to that given in the Casl Summary; it is repeated here for ease of reference.
Abstract: One of the most novel features of Casl, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of Casl specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by some details of the features provided in Casl for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.
Abstract: The way that refinement of individual "local" components of a specification relates to development of a "global" system from a specification of requirements is explored. Observational interpretation of specifications and refinements add expressive power and flexibility while bringing in some subtle problems. The results are instantiated in the context of Casl architectural specifications.
Abstract: Casl, the Common Algebraic Specification Language, has been designed by CoFI, the Common Framework Initiative for algebraic specification and development. Casl is an expressive language for specifying requirements and design for conventional software. It is algebraic in the sense that models of Casl specifications are algebras; the axioms can be arbitrary first-order formulas. This User Manual illustrates and discusses how to write Casl specifications.Casl is a major new algebraic specification language. It has been carefully designed by a large group of experts as a general-purpose language for practical use in software development - in particular, for specifying both requirements and design. Casl includes carefully-selected features from many previous specification languages, as well as some novel features that allow algebraic specifications to be written much more concisely and perspicuously than hitherto. It may ultimately replace most of the previous languages, and provide a common basis for future research and development.
Casl has already attracted widespread interest within the algebraic specification community, and is generally regarded as a de facto standard. Various sublanguages of Casl are available - primarily for use in connection with existing tools that were developed in connection with previous languages. Extensions of Casl provide languages oriented toward development of particular kinds of software (reactive, concurrent, etc.)
Major libraries of validated Casl specifications are freely available on the Internet, and the specifications can be reused simply by referring to their names. Tools are provided to support practical use of Casl: checking the correctness of specifications, proving facts about them, and managing the formal software development process.
The companion Casl Reference Manual [CoFI:2004:CASL-RM] provides full details of the Casl design, including its formal semantics.
Abstract: Component based design and development of software is one of the most challenging issues in software engineering. In this paper, we adopt a somewhat simplified view of software components and discuss how they can be conveniently modeled in a framework that provides a modular approach to formal software development by means of stepwise refinements. In particular we take into account an observational interpretation of requirements specifications and study its impact on the definition of the semantics of specifications of (parametrized) components. Our study is carried out in the context of Casl architectural specifications.
Abstract: In this paper we consider the partial many-sorted first-order logic and its extension to the subsorted partial many-sorted first-order logic that underly the Casl specification formalism. First we present counterexamples showing that the generalization of the Craig Interpolation Property does not hold for these logics in general (i.e., with respect to arbitrary signature morphisms). Then we formulate conditions under which the generalization of the Craig Interpolation Property holds for the first logic.
Abstract: In this paper we present the higher-order logic used in theorem-provers like the HOL system or Isabelle HOL logic as an institution. Then we show that for maps of institutions into HOL that satisfy certain technical conditions we can reuse the proof system of the higher-order logic to reason about structured specifications built over the institutions mapped into HOL. We also show some maps of institutions underlying the Casl specification formalism into HOL that satisfy conditions needed for reusing proof systems.
Abstract: We study proof systems for reasoning about logical consequences and refinement of structured specifications, based on similar systems proposed earlier in the literature. Following Goguen and Burstall, the notion of an underlying logical system over which we build specifications is formalized as an institution and extended to a more general notion, called (D,T)-institution. We show that under simple assumptions (essentially: amalgamation and interpolation) the proposed proof systems are sound and complete. The completeness proofs are inspired by proofs due to M. V. Cengarle for specifications in first-order logic and the logical systems for reasoning about them. We then propose a methodology for reusing proof systems built over institutions rich enough to satisfy the properties required for the completeness results for specifications built over poorer institutions where these properties need not hold.
Abstract: An environment for the Common Algebraic Specification Language Casl consists of several independent tools. A number of Casl tools have been built using the algebraic specification formalism Asf+Sdf and the Asf+Sdf Meta-Environment. Casl supports user-defined syntax which non-trivial to process: Asf+Sdf offers a powerful parsing technology (Generalized LR). Its interactive development environment facilitates rapid prototyping complemented bt early detection and correction of errors. A number of core technologies developed for the Asf+Sdf Meta-Environment can be reused in the context of Casl. Furthermore, an instantiaion of a generic format developed for the representation of Asf+Sdf specifications and terms provides a Casl-specific exchange format.
Abstract: How do distributed applications exchange tree-like data structures? We introduce the abstract data type of Annotated Terms (ATerms) and discuss their design, implementation and application. A comprehensive procedural interface enables creation and manipulation of ATerms in C or Java. The ATerm implementation is based on maximal subterm sharing and automatic garbage collection. A binary exchange format for the concise representation of ATerms (sharing preserved) allows the fast exchange of ATerms between applications. In a typical application - parse trees which contain considerable redundant information - less than 2 bytes are needed to represent a node in memory, and less than 2 bits are needed to represent it in binary format. The implementation of ATerms scales up to the manipulation of ATerms in the giga-byte range.
Abstract: This paper presents a permissive subsorted partial logic used in the CoFI Algebraic Specification Language. In contrast to other order-sorted logics, subsorting is not modeled by set inclusions, but by injective embeddings allowing for more general models in which subtypes can have different data type representations. Furthermore, there are no restrictions like monotonicity, regularity or local filtration on signatures at all. Instead, the use of overloaded functions and predicates in formulae is required to be sufficiently disambiguated, such that all parses have the same semantics. An overload resolution algorithm is sketched.
Abstract: The focus of this chapter is the incremental presentation of partial first-order logic, seen as a powerful framework where the specification of most data types can be directly represented in the most natural way. Both model theory and logical deduction are fully described. Alternatives to partiality, like (variants of) error algebras and order-sortedness, are also discussed, emphasizing their uses and limitations. Moreover, both the total and the partial (positive) conditional fragments are investigated in detail, and in particular the existence of initial (free) models for such restricted logical paradigms is proved. Finally some more powerful algebraic frameworks are sketched.
Abstract: In his 1995 book, M. Jackson introduces the concept of problem frame to describe specific classes of problems, to help in the specification and design of systems, and also to provide a framework for reusability. He thus identifies some particular frames, such as the translation frame (e.g., a compiler), the information system frame, the control frame (or reactive system frame), .... Each frame is described along three viewpoints that are application domains, requirements, and design. Our aim is to use Casl (or possibly a sublanguage or an extension of Casl if and when appropriate) to formally specify the requirements and the design of particular classes of problems ("problem frames"). This goal is related to methodology issues for Casl, that are here addressed in a more specific way, having in mind some particular problem frame, i.e., a class of systems. It is hoped that this will provide both a help in using, in a really effective way, Casl for system specifications, a link with approaches that are currently used in the industry, and a framework for the reusability. This approach is illustrated with some case studies, e.g., the information system frame is illustrated with the invoice system.
Abstract: Our approach aims at helping to produce adequate requirements, both clear and precise enough so as to provide a sound basis to the overall development. Our idea here is to find a way to combine both advantages of use cases and of formal specifications. We present a technique for improving use case based requirements, using the formally grounded development of the requirements specification, and that results both in an improved requirements capture, and in a requirement validation. The formally grounded requirements specification is written in a "visual" notation, using both diagrams and text, with a formal counterpart (written in the Casl and Casl-Ltl languages). Being formally grounded, our method is systematic, and it yields further questions on the system that will be reflected in the improved use case descriptions. The resulting use case descriptions are of high quality, more systematic, more precise, and its corresponding formally grounded specification is available. We illustrate our approach on part of the Auction System case study.
Abstract: One of the goals of software engineering is to provide what is necessary to write relevant, legible, useful descriptions of the systems to be developed, which will be the basis of successful developments. This goal was addressed both from informal approaches (providing in particular visual languages) and formal ones (providing a formal sound semantic basis). Informal approaches are often driven by a software development method, and while formal approaches sometimes provide a user method, it is usually aimed at helping to use the proposed formalism/language when writing a specification. Our goal here is to provide a companion method that helps the user to understand the system to be developed, and to write the corresponding formal specifications. We also aim at supporting visual presentations of formal specifications, so as to "make the best of both formal and informal worlds". We developed this method for the (logical-algebraic) specification languages Casl (Common Algebraic Specification Language, developed within the joint initiative CoFI) and for an extension for dynamic systems Casl-Ltl, and we believe it is general enough to be adapted to other paradigms. Another challenge is that a method that is too general does not encompass the different kinds of systems to be studied, while too many different specialized methods and paradigms result in partial views that may be difficult to integrate in a single global one. We deal with this issue by providing a limited number of instances of our method, fitted for three different kinds of software items and two specification approaches, while keeping a common "meta"-structure and way of thinking. More precisely, we consider here that a software item may be a simple dynamic system, a structured dynamic system, or a data structure. We also support both property-oriented (axiomatic) and model-oriented (constructive) specifications. We are thus providing support for the "building-bricks" tasks of specifying/modelling software artifacts that in our experience are needed for the development process. Our approach is illustrated with a lift case study, it was also used with other large case studies, and when used on projects by students yielded homogeneous results. Let us note that it may be used either as itself, e.g., for requirements specification, or in combination with structuring concepts such as the Jackson's problem frames.
Abstract: Casl, the Common Algebraic Specification Language, has been designed by CoFI, the Common Framework Initiative for algebraic specification and development. Casl is an expressive language for specifying requirements and design for conventional software. It is algebraic in the sense that models of Casl specifications are algebras; the axioms can be arbitrary first-order formulas.Casl is a major new algebraic specification language. It has been carefully designed by a large group of experts as a general-purpose language for practical use in software development - in particular, for specifying both requirements and design. Casl includes carefully-selected features from many previous specification languages, as well as some novel features that allow algebraic specifications to be written much more concisely and perspicuously than hitherto. It may ultimately replace most of the previous languages, and provide a common basis for future research and development.
Casl has already attracted widespread interest within the algebraic specification community, and is generally regarded as a de facto standard. Various sublanguages of Casl are available - primarily for use in connection with existing tools that were developed in connection with previous languages. Extensions of Casl provide languages oriented toward development of particular kinds of software (reactive, concurrent, etc.)
Major libraries of validated Casl specifications are freely available on the Internet, and the specifications can be reused simply by referring to their names. Tools are provided to support practical use of Casl: checking the correctness of specifications, proving facts about them, and managing the formal software development process.
This reference manual gives a detailed presentation of the Casl specification formalism. It reviews the main underlying concepts, and carefully summarizes the intended meaning of each construct of Casl. It formally defines both the syntax and semantics of Casl, and presents a logic for reasoning about Casl specifications. It also provides extensive libraries of Casl specifications of basic datatypes, and an annotated bibliography of CoFI publications.
Abstract: This part of the Casl Reference Manual gives a detailed summary of the syntax and intended semantics of Casl. Readers are assumed to be already familiar with the main concepts of algebraic specifications.Chapter 2 summarizes many-sorted basic specifications in Casl, which denote classes of many-sorted partial first-order structures: algebras where the functions are partial or total, and where also predicates are allowed. Axioms are first-order formulas built from equations and definedness assertions. Sort generation constraints can be stated. Datatype declarations are provided for concise specification of sorts together with constructors and (optional) selectors.
Chapter 3 summarizes subsorted basic specifications, which extend many-sorted specifications with a simple treatment of subsorts, interpreting subsort inclusion as embedding.
Chapter 4 summarizes structured specifications, which allow translation, reduction, union, and extension of specifications. Extensions may be required to be free; initiality constraints are a special case. A simple form of generic specifications is provided, together with instantiation involving parameter-fitting translations and views.
Chapter 5 summarizes architectural specifications, which define how the specified software is to be composed from a given set of separately-developed, reusable units with clear interfaces.
Chapter 6 summarizes specification libraries, which allow the (distributed) storage and retrieval of named specifications.
Finally, Chap. 7 (by Till Mossakowski) summarizes various sublanguages and extensions of Casl.
In general, each chapter first summarizes the main semantic concepts underlying the kind of specification concerned, then it presents the (abstract and concrete) syntax of the associated Casl language constructs and indicates their intended semantics. See Part II of this reference manual for complete grammars for the abstract and concrete syntax of Casl, and Part III for the formal semantics of Casl.
This summary does not attempt to motivate the design choices that have been taken; a rationale for a preliminary design has been published separately [Mosses:1997:CoFI], as has a full exposition of architectural specifications [Bidoit:2002:ASC]. See also [Astesiano:2002:CASL] for a concise overview of Casl, and [Bidoit:2004:CASL-UM] for a tutorial introduction.
Abstract: This part of the Casl Reference Manual is concerned with syntax. It makes the usual distinction between concrete syntax and abstract syntax: the former deals with the representation of specifications as sequences of characters, and with how these sequences can be grouped to form specifications, whereas the latter reflects only the compositional structure of specifications after they have been properly grouped.The abstract syntax of Casl plays a particularly central rôle: not only is it the basis for the Casl semantics, which is explained informally in Part I and defined formally in Part III, but also the abstract syntax of Casl specifications can be stored in libraries, so that tools can process the specifications without having to (re)parse them.
In acknowledgment of the importance of abstract syntax, consideration of concrete syntax for Casl was deferred until after the design of the abstract syntax - and of most of the details of its semantics - had been settled. The presentation of the Casl syntax here reflects the priority given to the abstract syntax:
- Chapter 2 specifies the abstract syntax of Casl;
- Chapter 3 gives a context-free grammar for Casl specifications, indicating also how ambiguities are resolved;
- Chapter 4 specifies the grouping of sequences of characters into sequences of lexical symbols, and determines their display format; and finally,
- Chapter 5 explains the form and use of comments and annotations (which are both included in abstract syntax, but have no effect on the semantics of specifications).
Abstract: A concrete dynamic-data type is just a partial algebra with predicates such that for some of the sorts there is a special predicate defining a transition relation.An abstract dynamic-data type (ad-dt) is an isomorphism class of such algebras. To obtain specifications for ad-dt's, we propose a logic which combines many-sorted first-order logic with branching-time combinators.
We consider both an initial and a loose semantics for our specifications and give sufficient conditions for the existence of the initial models. Then we discuss structured specifications and implementation.
Abstract: Software itself may be considered a formal structure and may be subject to mathematical analysis. This leads to a discipline of formal software engineering (which is not necessarily the same as the use of formal methods in software engineering), where a formal understanding of what software components are and how they may interact is used to engineer both the components themselves and their organisation. A strategy is using the concepts that are suited for organising the problem domain itself to organise the software as well. In this paper we apply this idea in the development of computational modeling software, in particular in the development of a family of related programs for simulation of elastic wave propagation in earth materials. We also discuss some data on the technique's effectiveness.
Abstract: The broader adoption of Casl will depend on its use being perceived as beneficial in the software development process. Traditionally the algebraic specifications community has focused on the use of algebraic methods for development of correct software within the standard waterfall software process model (and derivatives) for the implementation of software. Here we suggest a two-tiered softare process model, in which the first tier focuses on problem domain investigation and software architecture development, while the second tier is the implementation of software. Our experience has shown that algebraic methodology may play a significant role in the first tier, with significant improvements in software productivity as a result.
Abstract: The use of domain specific languages and appropriate software architectures are currently seen as the way to enhance reusability and improve software productivity. Here we outline a use of algebraic software methodologies and advanced program constructors to improve the abstraction level of software for scientific computing. This led us to the language of coordinate free numerics as an alternative to the traditional coordinate dependent array notation. We also sketch how the coordinate free language may be realised on a computer.
Abstract: In this paper we develop methods for verifying the correctness of architectural specifications, a mechanism introduced in the Casl specification language. This mechanism offers a formal way to express implementation steps in program development. Each such step states that to implement the unit of interest, one may implement some other units and then assemble them in the prescribed manner. In this paper we define a formal institution-independent semantics of architectural specifications, as well as sound and complete methods for proving them correct, applicable in the case of many institutions, in particular first-order logic.
Abstract: We present a proof-calculus for architectural specifications, complete w.r.t. their generative semantics. Architectural specifications, introduced in the Casl specification language, are a formal mechanism for expressing implementation steps in program development. They state that to implement a needed unit, one may implement some other units and then assemble them in the prescribed manner; thus they capture modular design steps in the development process. We focus on developing verification techniques applicable to full Casl architectural specifications, which involves, inter alia, getting around the lack of amalgamation in the Casl institution.
Abstract: Object-oriented modelling, using for instance the Unified Modeling Language (UML), is based on the principles of data abstraction and data encapsulation. In this paper, we closely examine the relationship between object-oriented models (using UML) and the classical algebraic approach to data abstraction (using the Common Algebraic Specification Language Casl). Technically, possible alternatives for a translation from UML to Casl are studied, and analysed for their principal consequences. It is shown that object-oriented approaches and algebraic approaches differ in their view of data abstraction. Moreover, it is explained how specification methodology derived from the algebraic world can be used to achieve highquality in object-oriented models.
Abstract: Based on a few concrete cases, we present a translation of UML class diagrams into Casl. The major difference w.r.t. other "algebraic" approaches is that this translation is intended to be integrated with translations of the other types of UML diagrams to Casl. The idea is that, while each kind of diagram has its own independent semantics, their semantics can be integrated to get an overall system description. In particular, the integration of the semantics of statecharts with class diagrams leads to a translation of operations in class diagrams to predicates instead of functions.
Abstract: Casl, a specification formalism developed recently by the CoFI group, offers architectural specifications as a way to describe how simpler modules can be used to construct more complex ones. The semantics for Casl architectural specifications formulates static amalgamation conditions as a prerequisite for such constructions to be well-formed. These are non-trivial in the presence of subsorts due to the failure of the amalgamation property for the Casl institution. We show that indeed the static amalgamation conditions for Casl are undecidable in general. However, we identify a number of practically relevant special cases where the problem becomes decidable and analyze its complexity there. In cases where the result turns out to be PSPACE-hard, we discuss further restrictions under which polynomial algorithms become available. All this underlies the static analysis as implemented in the Casl tool set.
Abstract: In this paper, we discuss the use of formal methods in the domain of geometric modeling. More precisely, the purpose of our work is to provide a formal specification language convenient for geometric modeling with tools. To do it, we are interested in a high-level operation, the chamfering with is already mathematically defined. Then we propose two specifications of it, using the two langages B and Casl, respectively representative of model-oriented approch and property-oriented approch. In order to as well as possible take advantage of the B and Casl characteristcs, we explicitly specify the chamfering in B and implicitly in Casl. In both cases, we succeded in providing a specification easily understandable by the experts of the application domain.
Abstract: This paper describes a case study to demonstrate the feasibility of successfully applying Casl to dedesing 3D geometric modeling softwares. Then it presents an abstract specification of a 3D geometric model, its basic constructive primitives and a hight-level operation: the chanfering one. We highlight the different useful Casl features for geometric modeling like free types or structured specifications. The resulting specification presents the advantages of being both abstract and helpful to easily write code.
Abstract: This paper presents an experiment that demonstrates the feasibility of successfully applying Casl to design 3D geometric modelling software. It presents an abstract specification of a 3D geometric model, its basic constructive primitives together with the definition of the rounding high-level operation. A novel methodology for abstractly specifying geometric operations is also highlighted. It allows one to faithfully specify the requirements of this specific area and reveals new mathematical definitions of geometric operations. The key point is to introduce an inclusion notion between geometric objects, in such a way that the result of an operation is defined as the smallest or largest object satisfying some pertinent criteria. This work has been made easier by using different useful Casl features, like first-order logic, free types or structured specifications. Some assets of this specification are to be abstract, readable by researchers in geometric modelling and simplify the programming process.
Abstract: La représentation mathématique des objets géométriques, la complexité et le nombre d'algorithmes nécessaire à leur manipulation, sont des indices forts pour une utilisation aisée et bénéfique des méthodes formelles. Nous présentons dans cet article une étude de la spécification formelle d'une opération complexe et importante en modélisation géométrique. Il s'agit de l'opération de chanfreinage consistant à arrondir les angles vifs des objets 3D. Cette étude est menée dans le cadre de deux méthodes formelles, B (orientée modèles) et Casl (orienté propriétés) dans l'objectif de privilégier la lisibilité par les experts du domaine. De plus, la formalisation et la rétro-ingénierie que nous avons réalisées, nous permettent de jeter les bases d'une méthodologie dédiée.
Abstract: The mathematical representation of geometric objects, the complexity and the number of algorithms necessary to handle them, make us believe that formal methodes are well suited to this field. In this article, we study the formal specification of tow important operations for geometric modelling: sewing and chanfering. Sewing consists in building a new object from two objects by joining them and chamfering is to flatten 3D objects' angles. We have used two formal methods, the B method (model oriented) and Casl (property oriented) in order to make it readable by the think-tank of the concerned field. Moreover, as realized formalisation and reengeneering we are able to lay foundations of dedicated methodology.
Abstract: The problem of testing modular systems against algebraic specifications is discussed. We focus on systems where the decomposition into parts is specified by a Casl-style architectural specification and the parts (units) are developed separately, perhaps by an independent supplier. We consider how to test such units without reference to their context of use. This problem is most acute for generic units where the particular instantiation cannot be predicted.
Abstract: We prove cocompleteness of the category of Casl signatures, of monotone signatures, of strongly regular signatures, and of strongly locally filtered signatures. This shows that using these signature categories is compatible with a pushout or colimit based module system.
Abstract: This paper presents a static semantic analysis for Casl, the Common Algebraic Specification Language. Abstract syntax trees are generated including subsorts and overloaded functions and predicates. The static semantic analysis, through the implementation of an overload resolution algorithm, checks and qualifies these abstract syntax trees. The result is a fully qualified Casl abstract syntax tree where the overloading has been resolved. This abstract syntax tree corresponds to a theory in the institution underlying Casl, subsorted partial first-order logic (SubPFOL). Two ways of embedding SubPFOL in higher-order logic (HOL) of the logical framework Isabelle are discussed: the first one from SubPFOL to HOL via PFOL (partial first-order logic) first drops subsorting and then partiality, and the second one is the counterpart via SubFOL (subsorted first-order logic). Finally, we sketch an integration of the embedding of Casl into the UniForM Workbench.
Abstract: We translate OBJ3 to Casl. At the level of basic specifications, we set up several institution representations between the underlying institutions. They correspond to different methodological views of OBJ3. The translations can be the basis for automated tools translating OBJ3 to Casl.
Abstract: Casl, the common algebraic specification language, has been developed as a language that subsumes many previous algebraic specification frameworks and also provides tool interoperability. Casl is a complex language with a complete formal semantics. It is therefore a challenge to build good tools for Casl. In this work, we present and discuss the Bremen Hol-Casl system, which provides parsing, static checking, conversion to LaTeX and theorem proving for Casl specifications. To make tool construction manageable, we have followed some guidelines: re-use of existing tools, interoperability of tools developed at different sites, and construction of generic tools that can be used for several languages. We describe the structure of and the experiences with our tool and discuss how the guidelines work in practice.
Abstract: We develop a notion of institution with symbols and a kernel language for writing structured specifications in Casl. This kernel language has a semantics in an arbitrary but fixed institution with symbols. Compared with other institution-independent kernel languages, the advantage is that translations, hidings etc. can be written in a symbol-oriented way (rather than being based on signature morphisms as primitive notion), while still being institution-independent. The semantics of the kernel language has been used as the basis for the semantics of structured specifications in Casl.
Abstract: Casl is a specification language combining first-order logic, partiality and subsorting. This paper generalizes the Casl logic to also include higher-order functions and predicates. The logic is presented in a modular step-by-step reduction: the logic is defined in terms of a generalized subsorted partial logic which in turn is defined in terms of many-sorted partial first-order logic. A new notion of homomorphism is introduced to meet the need to get a faithful embedding of first-order Casl into higher-order Casl. Finally, it is discussed how a proof calculus for the proposed logic can be developed.
Abstract: Development graphs are a tool for dealing with structured specifications in a way easing management of change and reusing proofs. In this work, we extend development graphs with hiding. Hiding is a particularly difficult to realize operation, since it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system.
Abstract: We describe a way to make the static analysis for the in-the-large part of the Common Algebraic Specification Language (Casl) independent of the underlying logic that is used for specification in-the-small. The logic here is formalized as an institution with some extra components. Following the institution independent semantics of Casl in-the-large, we thus get an institution independent static analysis for Casl in-the-large. With this, it is possible to re-use the Casl static analysis for extensions of Casl, or even completely different logics. One only has to provide a static analysis for specifications in-the-small for the given logic. This then can be plugged into the generic static analysis for Casl in-the-large.
Abstract: In this work, we investigate various specification languages and their relation to Casl, the recently developed Common Algebraic Specification Language. In particular, we consider the languages Larch, OBJ3 and functional CafeOBJ, ACT ONE, ASF, and HEP-theories, as well as various sublanguages of Casl. All these languages are translated to an appropriate sublanguage of Casl.The translation mainly concerns the level of specification in-the-small: the logics underlying the languages are formalized as institutions, and representations among the institutions are developed. However, it is also considered how these translations interact with specification in-the-large.
Thus, we obtain on the one hand translations of any of the abovementioned specification languages to an appropriate sublanguage of Casl. This allows us to take libraries and case studies that have been developed for other languages and re-use them in Casl.
On the other hand, we set up institution representations going from the Casl institution (and some of its subinstitutions) to simpler subinstitutions. Given a theorem proving tool for such a simpler subinstitution, with the help of a representation, it can also be used for a more complex institution. Thus, first-order theorem provers and conditional term rewriting tools become usable for Casl.
Abstract: We introduce CoCasl as a simple coalgebraic extension of the algebraic specification language Casl. CoCasl allows the nested combination of algebraic datatypes and coalgebraic process types. We show that the well-known coalgebraic modal logic and even the modal mu-calculus can be expressed in CoCasl. We present sufficient criteria for the existence of cofree models, also for several variants of nested cofree and free specifications. Moreover, we describe an extension of the existing proof support for Casl (in the shape of an encoding into higher-order logic) to CoCasl.
Abstract: Casl is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. Casl consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications (the latter are used to prescribe the structure of implementations).We describe an simplified version of the Casl syntax, semantics and proof calculus at each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a "black box", and similarly for the proof calculi. In particular, this means that Casl can easily be adapted to other logical systems.
Abstract: CoCasl, a recently defined coalgebraic extension of the algebraic specification language Casl, allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS and CSP, within such an algebraic-coalgebraic framework. It turns out that CoCasl can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structured operational semantics fit well in the algebraic world of Casl, while the additional coalgebraic constructs of CoCasl cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains.
Abstract: We provide a semantic basis for heterogeneous specifications that not only involve different logics, but also different kinds of translations between these. We show that Grothendieck institutions based on spans of (co)morphisms can serve as a unifying framework providing a simple but powerful semantics for heterogeneous specification.
Abstract: This part of the Casl Reference Manual provides proof calculi for the various levels of Casl specifications. It should be read together with the the Casl semantics (Part III).The aim of the Casl proof calculus is to support the users of Casl in the proof activities necessary in the process of software specification and development. Essentially, the goals are threefold. First, in a number of situations the model semantics for a Casl specification may fail even if the static semantics succeeds. This is the case for instance when a generic specification is instantiated with an actual parameter (which must then entail the formal parameter specification), when a view between two specifications is formed, or when a generic unit is applied to an argument in an architectural specification. One aim of the calculi developed here is to (make explicit and help the user to) discharge proof obligations such situations imply. Once this is done, we can be sure that the specification in question denotes a class of models. Then, the second aim of the calculi developed here is to prove consequences of such specifications - formulas that hold in all the models. Finally, this can be used to prove various relationships between Casl specifications.
Abstract: The Common Framework Initiative for Algebraic Specification (CoFI, pronounced like `coffee') is an open international collaboration. The main immediate aim is to design a coherent family of algebraic specification languages, based on a critical selection of constructs from the many previously-existing such languages - without sacrificing conceptual clarity of concepts and firm mathematical foundations. The long-term aims include the provision of tools and methods for supporting industrial use of the CoFI languages.After motivating the CoFI we outline its aims and scope, and sketch one general design decision that has already been taken.
Abstract: Casl is an expressive language for the algebraic specification of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). Casl combines the best features of many previous algebraic specification languages, and it is hoped that it may provide a focus for future research and development in the use of algebraic techniques, as well being attractive for industrial use.This paper presents Casl for users of the Asf+Sdf framework. It shows how familiar constructs of Asf+Sdf may be written in Casl, and considers some problems that may arise when translating specifications from Asf+Sdf to Casl. It then explains and motivates various Casl constructs that cannot be expressed directly in Asf+Sdf. Finally, it discusses the rôle that the Asf+Sdf system might play in connection with tool support for Casl.
Abstract: An open collaborative effort has been initiated: to design a common framework for algebraic specification and development of software. The rationale behind this initiative is that the lack of such a common framework greatly hinders the dissemination and application of research results in algebraic specification. In particular, the proliferation of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread acceptance throughout the research community is urgently needed.The aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The common framework will provide a family of specification languages at different levels: a central, reasonably expressive language, called Casl, for specifying (requirements, design, and architecture of) conventional software; restrictions of Casl to simpler languages, for use primarily in connection with prototyping and verification tools; and extensions of Casl, oriented towards particular programming paradigms, such as reactive systems and object-based systems. It should also be possible to embed many existing algebraic specification languages in members of the Casl family.
A tentative design for Casl has already been proposed. Task groups are studying its formal semantics, tool support, methodology, and other aspects, in preparation for the finalization of the design.
Abstract: Casl is an expressive language for the specification of functional requirements and modular design of software. It has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural specifications. Casl should facilitate interoperability of many existing algebraic prototyping and verification tools.This guided tour of the Casl design is based closely on a 1/2-day tutorial held at ETAPS'98 (corresponding slides are available from the CoFI archives). The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of Casl are briefly explained and illustrated--the reader is referred to the Casl Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.
Abstract: Casl, the Common Algebraic Specification Language, might be used as a meta-notation in action-semantic descriptions, instead of Unified Algebras. However, it appears that direct use of Casl as a meta-notation would have some drawbacks; a compromise is proposed.
Abstract: Casl is an expressive language for the algebraic specification of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). Casl combines the best features of many previous main-stream algebraic specification languages, and it should provide a focus for future research and development in the use of algebraic techniques, as well facilitating interoperability of existing and future tools.This paper presents Casl for users of the CafeOBJ framework, focussing on the relationship between the two languages. It first considers those constructs of CafeOBJ that have direct counterparts in Casl, and then (briefly) those that do not. It also motivates various Casl constructs that are not provided by CafeOBJ. Finally, it gives a concise overview of Casl, and illustrates how some CafeOBJ specifications may be expressed in Casl.
Abstract: CoFI, The Common Framework Initiative for algebraic specification and development of software, is an open international collaboration. The main initial aim of CoFI in 1995 was to design a coherent family of algebraic specification languages, based on a critical selection of constructs from the many previously-existing such languages - without sacrificing conceptual clarity of concepts and firm mathematical foundations. This aim was fulfilled in 1998 with the design of Casl, the Common Algebraic Specification Language, together with its sub-languages and extensions. The longer-term aims of CoFI include the provision of tools and methods for supporting industrial use of the Casl languages.
Abstract: We consider the problem of precisely defining UML active classes with an associated state chart. We are convinced that the first step to make UML precise is to find an underlying formal model for the systems modelled by UML. We argue that labelled transition systems are a sensible choice; indeed they have worked quite successfully for languages as Ada and Java. Moreover, we think that this modelization will help to understand the UML constructs and to improve their use in practice. Here we present the labelled transition system associated with an active class using the algebraic specification language Casl. The task of making precise this fragment of UML raises many questions about both the "precise" meaning of some constructs and the soundness of some allowed combination of constructs.
Abstract: We consider the problem of precisely defining UML active classes with an associated state chart. We are convinced that the first step to make UML precise is to find an underlying formal model for the systems modelled by UML. We argue that labelled transition systems are a sensible choice; indeed they have worked quite successfully for languages as Ada and Java. Moreover, we think that this modelization will help to understand the UML constructs and to improve their use in practice. Here we present the labelled transition system associated with an active class using the algebraic specification language Casl. The task of making precise this fragment of UML raises many questions about both the "precise" meaning of some constructs and the soundness of some allowed combination of constructs
Abstract: We discuss the nature of the semantics of the UML. Contrary to the case of most languages, this task is far from trivial. Indeed, not only the UML notation is complex and its informal description is incomplete and ambiguous, but we also have the UML multiview aspect to take into account. We propose a general schema of the semantics of the UML, where the different kinds of diagrams within a UML model are given individual semantics and then such semantics are composed to get the semantics on the overall model. Moreover, we fill part of such a schema, by using the algebraic language Casl as a metalanguage to describe the semantics of class diagrams, state machines and the complete UML formal systems.
Abstract: Casl the basic language developed within CoFI, the Common Framework Initiative for algebraic specification and development, cannot be used for specifying the requirements and the design of dynamic software systems. Casl-Ltl is an extension to overcome this limit, allowing to specify dynamic system by modelling them by means of labelled transition systems and by expressing their properties with temporal formulae. It is based on LTL, the Labelled Transition Logic, that is a logic-algebraic formalism for the specification of dynamic systems, mainly developed by E. Astesiano and G. Reggio (see [Astesiano:2001:LTL] and [Costa:1997:SAD]). This document gives a detailed summary of the syntax and intended semantics of Casl-Ltl. It is intended for readers who are already familiar with Casl [Bidoit:2004:CASL-UM]. Four short examples are given in the appendix, and extended case studies using Casl-Ltl are given in [Choppy:1999:UCS,Choppy:2003:TFG]. An extensive companion user method is given in [Choppy:2003:TFG] (while [Choppy:2000:UCS] gives a first attempt to rely on structuring concepts). Casl-Ltl was also used to present the semantics of some parts of UML in [Reggio:2000:AUA,Reggio:2001:RSU].
Abstract: We present a weak theory BasicReal of the real numbers in the first order specification language Casl. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. BasicReal captures for instance e and pi as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype BasicReal and specifications of the real numbers in higher order logic and various set theories.
Abstract: This part of the Casl reference manual describes a library of elementary specifications called the Basic Datatypes. This library has been developed with two main purposes in mind: on the one hand, it provides the user with a handy set of off-the-shelf specifications to be used as building blocks in the same way as library functions in a programming language, thus avoiding continuous reinvention of the wheel. On the other hand, it serves as a large reservoir of example specifications that illustrate both the use of Casl at the level of basic and structured specifications.The name Basic Datatypes is actually slightly misleading in that there are both monomorphic specifications of typical datatypes and loose specifications that express properties e.g. of an algebraic or order theoretic nature. The first type of specification includes simple datatypes like numbers and characters as well as structured datatypes (typically involving type parameters) such as lists, sets, arrays, or matrices. The second type of specification is oriented more closely towards traditional mathematical concepts; e.g. there are specifications of monoids and rings, as well as equivalence relations or partial orders. The library is structured partly along precisely these lines; an overview of the sublibraries is given in Sect. 1.1.
In the design of a library of basic specifications, there is a certain amount of tension between the contradicting goals of
This concerns in particular the degree of structuring, with parametrized specifications being most prominent as on the one hand increasing elegance and reusability and on the other hand placing on the reader the burden of looking up imported specifications and keeping track of signature translations. With the exception of the library of numbers, the libraries exhibit a certain bias towards more extensive use of structuring operations. Several measures have been undertaken to enhance readability of the specifications, one of them being the facility to have the signatures for the specifications in a library explicitly listed by the Casl tools.
- keeping specifications simple and readable also for novice users, and
- making them economical, concise, and amenable for tool support.
The specifications make use of a set of annotations concerning semantics and operator precedences; moreover, we use the Casl syntax for literals. The details of these annotations and syntax extensions are explained in Chap. II:5. of the Casl Language Syntax.
The material is organized as follows. After the above-mentioned descriptions of the component libraries (Section 1.1), the actual content of the libraries is presented in Chaps. 2-11. Chapter 12 contains graphical representations of the dependencies between the specifications. Moreover, there is an index of all library and specification names at the end of the book.
Abstract: Various formalizations of the concept of "refinement step" as used in the formal development of programs from algebraic specifications are presented and compared.
Abstract: The Common Framework Initiative (CoFI) is an open international collaboration which aims to provide a common framework for algebraic specification and development of software. The central element of the Common Framework is a specification language called Casl for formal specification of functional requirements and modular software design which subsumes many previous algebraic specification languages. This paper is a brief summary of past and present work on CoFI.
Abstract: We construct a representation of the institution of the algebraic specification language Casl in an institution called enriched Casl. Enriched Casl satisfies the amalgamation property, which fails in the Casl institution, as well as its converse. Thus, the previously suggested institution-independent semantics of architectural specifications is actually applicable to Casl. Moreover, a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for Casl.
Abstract: We present a semantics for architectural specifications in Casl, including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for Casl models. To circumvent this problem, we extend the Casl logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor has amalgamation, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Concretizing to the Casl institution, we discuss a calculus for discharging the static amalgamation conditions. These are in general undecidable, but can be dealt with by approximative algorithms in all practically relevant cases.
Abstract: The specification of programs in modern functional languages such as Haskell requires a specification language that supports the type system of these languages, in particular higher order types, type constructors, and parametric polymorphism. We lay out the design of HasCasl, a higher order extension of the algebraic specification language Casl that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order Casl. The number of primitive concepts in the logic has been kept as small as possible; we demonstrate how various extensions to the logic can be formulated within the language itself.
Abstract: Along the lines of classical categorical type theory for total functions, we establish correspondence results between certain classes of partial equational theories on the one hand and suitable classes of categories having certain finite limits on the other hand. E.g., we show that finitary partial theories with existentially conditioned equations are essentially the same as cartesian categories with distinguished domains, and that partial lambda-theories with internal equality are equivalent to a suitable class of partial cartesian closed categories.
Abstract: We define (set-theoretic) notions of intensional Henkin model and syntactic lambda-algebra for Moggi's partial lambda-calculus. These models are shown to be equivalent to the originally described categorical models via the global element construction; the proof makes use of a previously introduced construction of classifying categories. The set-theoretic semantics thus obtained is the foundation of the higher order algebraic specification language HasCasl, which combines specification and functional programming.
Abstract: Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. As the background formalism for these concepts, we use the logic of HasCasl, a higher-order language for functional specification and programming.
Abstract: Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. It is thus natural to develop a Hoare calculus for reasoning about computational monads. While this has previously been done only for the state monad, we here provide a generic, monad-independent approach, which applies also to further computational monads such as exceptions, input/output, and non-determinism. All this is formalized within the logic of HasCasl, a higher-order language for functional specification and programming. Combination of monadic features can be obtained by combining their loose specifications. As an application, we prove partial correctness of Dijkstra's nondeterministic version of Euclid's algorithm in a monad with nondeterministic dynamic references.
Abstract: We present a semantics for architectural specifications in Casl, including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for Casl models. To circumvent this problem, we extend the Casl logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched Casl means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for Casl.
Abstract: Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. As the background formalism for these concepts, we use the logic of HasCasl, a higher-order language for functional specification and programming. As an example application, we develop a monad-independent Hoare calulus for total correctness based on our dynamic logic, and illustrate this calculus by a termination proof for Dijkstra's non-deterministic implementation of Euclid's algorithm.
Abstract: This paper presents an overview of abstract specification theory, as understood and viewed by the author. We start with a brief outline of the basic assumptions underlying work in this area in the tradition of algebraic specification and with a sketch of the algebraic and categorical foundations for this work. Then, we discuss the issues of specification construction and of systematic development of software from formal requirements specification. Special attention is paid to architectural design: formal description of the modular structure of the system under development, as captured by architectural specifications in Casl. In particular, we present a simplified but representative formalism of architectural specifications with complete semantics and verification rules. We conclude by adapting the ideas, concepts and results presented to the observational view of software systems and their specification.