Volume 22, 2003, No. 3

The Expressive Power of Abstract-State Machines

W. REISIG   Abstract Conventional computation models assume symbolic representations of states and actions. Gurevich's ``Abstract-State Machine'' model takes a more liberal position: Any mathematical structure may serve as a state. This results in ``a computational model that is more powerful and more universal than standard computation models''. We characterize the Abstract-State Machine model as a special class of transition systems that widely extends the class of ``computable'' transition systems. This characterization is based on a fundamental Theorem of Y. Gurevich.

 

Foundations of the B method

D. CANSELL, D. MÉRY   Abstract B is a method for specifying, designing and coding software systems. It is based on Zermelo-Fraenkel set theory with the axiom of choice, the concept of generalized substitution and on structuring mechanisms (machine, refinement, implementation). The concept of refinement is the key notion for developing B models of (software) systems in an incremental way. B models are accompanied by mathematical proofs that justify them. Proofs of B models convince the user (designer or specifier) that the (software) system is effectively correct. We provide a survey of the underlying logic of the B method and the semantic concepts related to the B method; we detail the B development process partially supported by the mechanical engine of the prover.

 

CafeOBJ: Logical Foundations and Methodologies
	R. DIACONESCU, K. FUTATSUGI, K. OGATA   Abstract CafeOBJ is an executable industrial strength multi-logic algebraic specification language which is a modern successor of OBJ and incorporates several new algebraic specification paradigms. In this paper we survey its logical foundations and present some of its methodologies.

 

Casl --- The Common Algebraic Specification Language: Semantics and Proof Theory

T. MOSSAKOWSKI, A. E. HAXTHAUSEN, D. SANNELLA, A. TARLECKI   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.

 

Volume 22, 2003, No. 3