SAS Journals

Scientific Journals and Yearbooks Published at SAS

Article List

Computing and Informatics

Volume 22, 2003, No. 3-4

Content:

REISIG, W.
The Expressive Power of Abstract-State Machines.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 209-219.
CANSELL, D. - MERY, D.
Foundations of the B method.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 221-256.
DIACONESCU, R. - FUTATSUGI, K. - OGATA, K.
CafeOBJ: Logical Foundations and Methodologies.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 257-283.
MOSSAKOWSKI, T. - HAXTHAUSEN, A. - SANNELLA, D. - TARLECKI, A.
CASL --- The Common Algebraic Specification Language: Semantics and Proof Theory.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 285-321.
GEORGE, C. - E. HAXTHAUSEN, A.
The Logic of the RAISE Specification Language.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 323-350.
MERZ, S.
On the Logic of TLA+.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 351-379.
C. HENSON, M. - REEVES, S. - P. BOWEN, J.
Z Logic and its Consequences.
In Computing and Informatics. Vol. 22, no. 3-4 (2003), p. 381-415.

	The Expressive Power of Abstract-State Machines W. REISIG 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. Computing and Informatics. Volume 22, 2003, No. 3-4: 209-219.
	Foundations of the B method DOMINIQUE CANSELL, DOMINIQUE MERY Events, actions, systems, refinement, proof, validation, formal method 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. Computing and Informatics. Volume 22, 2003, No. 3-4: 221-256.
	CafeOBJ: Logical Foundations and Methodologies RAZVAN DIACONESCU, KOKICHI FUTATSUGI, KAZUHIRO OGATA CafeObj, algebraic specification, institutions, absrtract machines 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. Computing and Informatics. Volume 22, 2003, No. 3-4: 257-283.
	CASL --- The Common Algebraic Specification Language: Semantics and Proof Theory TILL MOSSAKOWSKI, ANNE E. HAXTHAUSEN, DONALD SANNELLA, ANDRZEJ. TARLECKI Algebraic specification, formal software development, logic, calculi, institutions 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. Computing and Informatics. Volume 22, 2003, No. 3-4: 285-321.
	The Logic of the RAISE Specification Language CHRIS GEORGE, ANNE E. HAXTHAUSEN Formal methods, logics, RAISE This paper describes the logic of the RAISE Specification Language, RSL. It explains the particular logic chosen for RAISE, and motivates this choice as suitable for a wide spectrum language to be used for designs as well as initial specifications, and supporting imperative and concurrent specifications as well as applicative sequential ones. It also describes the logical definition of RSL, its axiomatic semantics, as well as the proof system for carrying out proofs. Computing and Informatics. Volume 22, 2003, No. 3-4: 323-350.
	On the Logic of TLA+ STEPHAN MERZ Temporal logic, reactive systems, specification. verification, refinement TLAp is a language intended for the high-level specification of reactive, distributed, and in particular asynchronous systems. Combining the linear-time temporal logic TLA and classical set-theory, it provides an expressive specification formalism and supports assertional verification. Computing and Informatics. Volume 22, 2003, No. 3-4: 351-379.
	Z Logic and its Consequences MARTIN C. HENSON, STEVE REEVES, JONATHAN P. BOWEN Formal methods, specification language, logic, Z This paper provides an introduction to the specification language Z from a logical perspective. The possibility of presenting Z in this way is a consequence of a number of joint publications on Z logic that Henson and Reeves have co-written since 1997. We provide an informal as well as formal introduction to Z logic and show how it may be used, and extended, to investigate issues such as equational logic, the logic of preconditions, the issue of monotonicity and both operation and data refinement. Computing and Informatics. Volume 22, 2003, No. 3-4: 381-415.