Paper on a state-based extension of CASL

[Hubert Baumeister <baumeist@informatik.uni-muenchen.de>]

Dear all,

Sascha and I have just finished the paper

        State-Based Extension of CASL

which describes an extension of CASL based on the state-as-algebra
approach. The extension brings
together ideas from Gurevich's Abstract State Machines, the Implicit
State Approach, d-oids, and Z.

The paper is available at:

        http://www.informatik.uni-muenchen.de/~baumeist/ifm2000.ps.gz

Greetings,
        Hubert Baumeister

Abstract:

A state-based extension of the algebraic specification language 
CASL is presented. It permits the specification of the static 
part of a complex dynamic system by means of CASL and the dynamic 
part by means of the facilities described in the paper. The 
dynamic system is defined as possessing a number of states and a 
number of operations (procedures) for transforming one state into 
another. Each state possesses one and the same static part 
specified by CASL and a varying part specified by additional 
tools. The varying part includes dynamic 
sorts/functions/predicates and dependant functions/predicates. 
The dependant functions/predicates are specified by formulae 
using the names of the dynamic functions/predicates so that each 
time one of the last ones is updated the corresponding former 
ones are also updated. The updates of the dynamic entities are 
produced by procedures which are specified by means of 
preconditions, postconditions and dynamic equations. 


-- 
Hubert Baumeister, LMU M"unchen, Institut f"ur Informatik
mailto:baumeist@informatik.uni-muenchen.de
http://www.informatik.uni-muenchen.de/~baumeist
phone (x49-89)2178-2177  * fax -2175