This document is available in various formats from the CoFI archives at ftp://ftp.brics.dk/Projects/CoFI/Bibliography/Annotated/.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 annotations. See the changes document for a list of changes.The abbreviated bibliography and the unabbreviated bibliography list the same references as this bibliography, as does the list of abstracts. The cross-referenced proceedings and books are listed separately.
Proposes an extension of Casl with methods, which are special functions s.t. overloading resolution for them is delayed to evaluation time and is not required to be conservative.
Discusses the relationship between Casl and programming languages.
The paper presents some initial ideas about the formalization of the UML.
Presents a survey of the algebraic methods for the specification of concurrent systems, using a common simple example, and classifying them in four kinds.
Presents an approach for the composition of languages, in particular a data description language and a paradigm-specific language, exemplified by sketching how to combine UML and a data language.
Outlines a logical (algebraic) method for the specification of reactive/distributed systems both at the requirement and at the design level, providing references for detailed presentations of single aspects and applications.
Gives an overview of the Casl design, indicating major issues, and explaining main concepts and constructs. Compares Casl to some other major algebraic specification languages.
Defines a translation of a subset of Casl into the notion of development graphs, in order to maintain evolving Casl specifications.
Explains the Maya system, which maintains structured specifications and their proofs with the help of development graphs.
Maya provides management of proofs for structured specifications; Hol-Casl is a prover for Casl basic specifications. Here, these two are combined
Explains the basic features of Casl specifications using the warehouse case study.
Defines an institution for the logic underlying Z. Shows a translation of Z-schemata to abstract datatypes over that institution.
Presents an extension of Casl for writing model-oriented specifications. The extension is based on the state-as-algebra approach.
Presents the complete semantics of Casl in natural semantics style.
Presents a set of algebraic operators in Casl to create complex scenarios. Provides a semantics in a temporal model and shows how to derive some properties of the scenarios.
Motivates and presents Casl architectural specifications.
Gives an informal motivation for and presentation of Casl architectural specifications, with hints on their semantics and use in the development process.
Studies development steps that apply local constructions in a global context, and gives the semantics of a version of Casl architectural specifications, including their observational interpretation.
Illustrates and discusses how to write Casl specifications, with additional chapters on foundations, tools, and libraries, a realistic case study, and a quick-reference overview of Casl.
Provides a light-weight introduction to [Bidoit:2002:GDL], with an illustrative example.
Gives a proof of the Craig Interpolation Property for the partial many-sorted first-order logic, underlying Casl. This property is crucial for results presented in [ann-Borzyszkowski:2002:LSS].
Formulates conditions under which we can reuse the HOL logic to reason about structured specifications built over institutions mapped into HOL. It works also for the structured part of Casl.
Presents completeness results for proof systems for structured specifications. Also introduces a methodology for reusing complete proof systems for systems that are not complete.
Describes the architecture of a Casl parser based on the SGLR parsing technology developed for Asf+Sdf, and discusses the mapping to abstract syntax trees represented as ATerms.
Describes an efficient and generic representation of tree-like data structures, and reports on several case studies, including the abstract syntax of Casl.
Provides an overview of the state of the art in algebraic specification at the end of the 90's, with a comprehensive bibliography. Discusses semantics, structuring constructs, specific algebraic paradigms, methodology issues, and existing tools.
Presents the permissive subsorted partial logic used in the Casl semantics.
Presents partial first-order logic, both model theory and logical deduction. Compares partial specifications to error algebras and order-sortedness.
Shows how formal specification skeletons may be associated with the structuring concepts provided by M. Jackson's Problem Frames, used to provide a first gross structure and characterization of the system under study.
Shows how formal specification skeletons may be associated with the structuring concepts provided by M. Jackson's Problem Frames, used to provide a first gross structure and characterization of the system under study.
Presents guidelines for writing (and meanwhile understanding) descriptions/specifications, both in property-oriented and model-oriented styles. Provides visual descriptions, and formal specifications in Casl-Ltl.
Presents a technique for improving use case based requirements, using the formally grounded development of the requirements specification (in Casl and Casl-Ltl).
Gives full details of the design of Casl: an informal language summary, concrete and abstract syntax, well-formedness and model-class semantics, and proof rules. Includes the libraries of basic datatypes.
Gives an informal summary of the Casl constructs for basic, structured, architectural, and library specifications. Defines sublanguages and lists proposed extensions of Casl.
Defines the lexical, concrete, and abstract syntax of Casl.
JTN is a formal graphic notation for Java-targeted design specifications (i.e., of systems that will be implemented using Java).
Proposes a logic which combines many-sorted first-order logic with branching-time combinators for the specification of dynamic-data types.
Descripes the development of a software family for seismic simulations. Algebraic methods are used for domain and software architecture engineering. Quantitative estimates of the benefits are made.
Describes a software process model where Casl is used for domain engineering.
Presents the notion of algebraic software methodologies and their use for domain engineering and software architecture design.
Defines and discusses static and model semantics of architectural specifications, as well as a semantics for programs and a verification semantics, which makes use of so-called sharing maps.
Develops techniques for verifying architectural specifications w.r.t. a non-generative semantics for institutions with logical amalgamation, obtaining full verification for first-order logic.
Presents an institution-independent proof-calculus for architectural specifications, complete w.r.t. a generative semantics, and applies it to the full Casl institution.
Case study in HasCasl. Graphs and Petri nets become first-class citizens and can be used as tokens in Petri nets.
Examines the relationship between object-oriented models (using UML) and the classical algebraic approach to data abstraction (using Casl).
Introduces step by step a semantic translation of UML class diagrams into Casl specifications in a way that the result may be integrated with the semantics of other kinds of diagrams.
Presents state-of-the art surveys of the major research topics in the area of algebraic specifications, written by leading experts in the field.
Describes algorithmic aspects of static analysis of Casl, including the cell calculus for architectural specifications.
Provides static analysis for Casl architectural specifications with cell calculus.
Gives a first comparison of using Casl and the B method on the chamfering operation in topology-based modeling.
Provides a Casl case study in geometric modeling and presents the different useful Casl features for geometric modeling.
Gives a specification methodology dedicated to topology-based modeling. This methodology is commented and illustrated with several examples.
Gives a complete case study of using Casl and the B method in topology-based modeling. Includes foundations of dedicated methodology.
An extended version of [Ledoux:2001:SFC]. Gives a complete case study of using Casl and the B method in topology-based modeling. Includes foundations of dedicated methodology.
Studies the problem of testing modular systems against Casl architectural specifications, focussing on unit testing.
Proves cocompleteness of the Casl signature category and explains the relation to order-sorted algebra.
Describes the Casl tool set, including the overload resolution algorithm and encodings to higher-order logic.
Presents different translations of OBJ3 to Casl, using different treatments of OBJ3's total retracts.
Gives a description of the Casl tool set and the Hol-Casl theorem prover.
Adds symbols to institutions, needed for Casl symbol maps.
This was the first proposal for a higher-order extension of Casl, superseded by HasCasl [Schroeder:2002:HIS].
Presents the kernel formalism for structured theorem proving that is used in the Casl proof calculus.
Makes the Casl tool set as much institution independent as possible.
Provides translations from other specification languages to Casl, as well as translations among sublanguages, including those needed for the Casl tool set.
Proposes a coalgebraic extension of Casl, including cogenerated, simple and structured cofree and modal logic.
Presents a case study in CoCasl, specifying CCS and CSP coalgebraically.
Provides a semantics for heterogeneous specifications involving both different institutions and institution translations of different kinds.
Gives an overview of a simplified version of the Casl syntax, semantics and proof calculus, for basic, structured and architectural specifications.
Presents proof calculi that support reasoning about Casl specifications; proves soundness and discusses completeness.
Presents CoFI, describing the aims and goals.
Gives an overview of Casl, comparing it to Asf+Sdf.
Describes a tentative design for Casl, motivating some of the design choices.
Indicates the major issues in the Casl design, explains and illustrates the main concepts and constructs. Based on a 1/2-day tutorial.
Gives an overview of Casl, and considers pros and cons of using it as meta-notation in action semantic descriptions of programming languages.
Gives an overview of Casl, comparing it to CafeOBJ.
Describes the aims, goals, and initial achievements of CoFI, extending and updating [Mosses:1996:CoFI].
Describes the Casl-Ltl extension language proposed for dynamic systems specification, with dynamic sorts and temporal formulas.
Presents the labelled transition system associated with an active class using Casl.
Presents the labelled transition system associated with an active class using Casl.
Using Casl as a metalanguage, proposes a semantics for class diagrams, state machines and overall systems described using the UML.
Presents the labelled transition system associated with an active class using Casl.
Presents a combination of statecharts and Casl.
Presents the complete syntax and semantics of a combination of statecharts and Casl.
Using Casl as a metalanguage, proposes a semantics for class diagrams, state machines and overall systems described using the UML.
Describes the Casl-Ltl extension language proposed for dynamic systems specification, with dynamic sorts and temporal formulae.
Presents a weak first-order theory of real numbers in Casl.
Introduces a calculus for proving consistency of Casl specifications; the syntax-driven approach exploits in particular the Casl structuring operations
Describes the integration of the process algebra CSP and the algebraic specification language Casl into one language, with denotational semantics in the process part and loose semantics for the datatypes.
Provides libraries of basic datatypes in Casl, including order-theoretic and basic algebraic concepts, simple and structured datatypes, and graphs.
Advocates a formalism which combines the CCS process algebra with the Casl algebraic specification language, presents formal foundations of this combination, and illustrates it with a real size case study: an access control system to a set of buildings.
Provides an overview of formal algebraic notions of refinement step.
Gives an overview of CoFI, with emphasis on the features of Casl.
Reports on progress with CoFI during 1998-2001.
Presents definition of and results about enriched Casl, which restores the lacking amalgamation property.
Solves the problems of Casl architectural specifications with subsorts by introducing enriched Casl and a diagram static semantics.
The central paper explaining HasCasl, a higher-order extension of Casl including type constructors, polymorphism and recursion.
Establishes correspondence results between partial equational theories, of which Casl signatures are a special case, and categories with certain finite limits, in preparation for the semantics of HasCasl.
Shows that categorical models of the partial lambda-calculus and intensional Henkin models, as used in the semantics of HasCasl, are equivalent
Monad-independent dynamic logic in the framework of HasCasl; admits reasoning about termination and total correctness.
Hoare logic for arbitrary monads (e.g., exceptions, non-determinism, references, input/output) in the framework of HasCasl.
Solves the problems of Casl architectural specifications with subsorts by introducing enriched Casl and a diagram static semantics.
Monad-independent dynamic logic in the framework of HasCasl; admits reasoning about termination, partial and total correctness.
Provides an overall view of abstract specification and software development theory, including a version of Casl architectural specifications with an example, semantics and verification rules.