Titlebook: Algebra, Meaning, and Computation; Essays dedicated to Kokichi Futatsugi,Jean-Pierre Jouannaud,José Meseg Book 2006 Springer-Verlag Berlin

ANA

热情的我

From OBJ to Maude and Beyondign. A common thread is the quest for ever more expressive computational logics, on which executable formal specifications of increasingly broader classes of systems can be based. Several recent extensions, beyond Maude itself, are also discussed.

废止

Constructive Action Semantics in OBJcould be improved. We propose using the notation and modular structure of the Constructive Action Semantics framework in OBJ, and give a simple illustration. The reader is assumed to be familiar with OBJ.

mechanism

languid

Composition by Colimit and Formal Software Developmenty of situations in which colimits can be mechanically applied to support software development by refinement. We illustrate the use of colimits to support automated datatype refinement, algorithm design, aspect weaving, and security policy enforcement.

PURG

Proving Behavioral Refinements of COL-specificationsnted properties of software systems. In this paper we consider behavioral refinement relations between COL-specifications taking into account implementation constructions. We propose a general strategy for proving the correctness of such refinements by reduction to (standard) first-order theorem pro

抗原

扩大

Kokichi Futatsugi,Jean-Pierre Jouannaud,José MesegIncludes supplementary material:

COMMA

Lecture Notes in Computer Sciencehttp://image.papertrans.cn/a/image/152542.jpg

突袭