Common Algebraic Specification Language
Encyclopedia
The Common Algebraic Specification Language (CASL) is a general-purpose specification language
based on first-order logic
with induction
. Partial function
s
and subsorting
are also supported.
CASL has been designed by CoFI, the Common Framework Initiative, with the aim to subsume
many existing specification languages.
CASL comprises four levels:
The four levels are orthogonal to each other. In particular, it is possible to use CASL structured and architectural
specifications
and libraries with logics other than CASL. For this purpose, the logic has to be formalized as an institution
. This feature is also used by the CASL extensions.
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
based on first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
with induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
. Partial function
Partial function
In mathematics, a partial function from X to Y is a function ƒ: X' → Y, where X' is a subset of X. It generalizes the concept of a function by not forcing f to map every element of X to an element of Y . If X' = X, then ƒ is called a total function and is equivalent to a function...
s
and subsorting
Subtype
In programming language theory, subtyping or subtype polymorphism is a form of type polymorphism in which a subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program constructs, typically subroutines or functions, written to operate on...
are also supported.
CASL has been designed by CoFI, the Common Framework Initiative, with the aim to subsume
Subsumption architecture
Subsumption architecture is a reactive robot architecture heavily associated with behavior-based robotics. The term was introduced by Rodney Brooks and colleagues in 1986...
many existing specification languages.
CASL comprises four levels:
- basic specifications, for the specification of single software modules,
- structured specifications, for the modular specification of modules,
- architectural specifications, for the prescription of the structure of implementationImplementationImplementation is the realization of an application, or execution of a plan, idea, model, design, specification, standard, algorithm, or policy.-Computer Science:...
s, - specification libraries, for storing specifications distributed over the InternetInternetThe Internet is a global system of interconnected computer networks that use the standard Internet protocol suite to serve billions of users worldwide...
.
The four levels are orthogonal to each other. In particular, it is possible to use CASL structured and architectural
Software architecture
The software architecture of a system is the set of structures needed to reason about the system, which comprise software elements, relations among them, and properties of both...
specifications
Algebraic specification
Algebraic specification, is a software engineering technique for formally specifying system behavior. Algebraic specification seeks to systematically develop more efficient programs by:...
and libraries with logics other than CASL. For this purpose, the logic has to be formalized as an institution
Institution (computer science)
The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970sin order to deal with the "population explosion among the logical systems used incomputer science"...
. This feature is also used by the CASL extensions.
Extensions
Several extensions of CASL have been designed:- HasCASL, a higher-orderHigher-order logicIn mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
extension - CoCASL, a coalgebraicF-coalgebraIn mathematics, specifically in category theory, an F-coalgebra is a structure defined according to a functor F. For both algebra and coalgebra, a functor is a convenient and general way of organizing a signature...
extension - CspCASL, a concurrentConcurrency (computer science)In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
extension based on CSPCommunicating sequential processesIn computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi... - ModalCASL, a modal logicModal logicModal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
extension - CASL-LTL, a temporal logicTemporal logicIn logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
extension - HetCASL, an extension for heterogeneous specification