The Common Algebraic Specification Language (CASL) is a general-purpose specification language based on first-order logic with induction. Partial functions and subsorting are also supported. A specification language is a formal language used in computer science. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers, or otherwise is true of all members of an infinite sequence. ... In mathematics and computer science, a partial function from the domain X to the codomain Y is a binary relation over X and Y which associates with every element in the set X at most one element in the set Y. If a partial function associates with every element in... ...

CASL has been designed by CoFI, the Common Framework Initiative, with the aim to subsume many existing specification languages.

CASL comprises of 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 implementations,
• specification libraries, for storing specifications distributed over the Internet.

The four levels are orthogonal to each other. In particular, it is possible to use CASL structured and architectural specifications and libraries also with other logics than the CASL logic. For this purpose, the logic has to be formalized as an institution. This provides also the basis for CASL extensions. In engineering and computer science, an implementation is the practical application of a method or algorithm to fulfill a desired purpose. ... The notion of institution has been created by Joseph Goguen and Rod Burstall in the early 1980s in order to deal with the population explosion among the logical systems used in computer science. The notion tries to capture the essence of what a logical system is. ...

Extensions

Several extensions of CASL have been designed:

• HasCASL, a higher-order extension
• CoCASL, a coalgebraic extension
• CspCASL, a concurrent extension based on CSP
• ModalCASL, a modal logic extension
• CASL-LTL, a temporal logic extension
• HetCASL, an extension for heterogeneous specification

In mathematics, higher-order logic is distinguished from first-order logic in a number of ways. ... In mathematics, coalgebras are structures that are in a certain sense dual to the unital associative algebras. ... In computer science, concurrency is concerned with computation that makes parallel use of shared resources that can change. ... In computer science, Communicating Sequential Processes (CSP) is a language for describing patterns of interaction. ... Modal logic, or (less commonly) intensional logic is the branch of logic that deals with sentences that are qualified by modalities such as can, could, might, may, must, possibly, and necessarily, and others. ... In 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. ... This page is a candidate to be moved to Wiktionary. ...

Links

• Official CoFI website
• CASL at the University of Bremen
• Hets, the main analysis tool for CASL