Titlebook: Software Engineering with OBJ; Algebraic Specificat Joseph Goguen,Grant Malcolm Book 2000 Springer Science+Business Media New York 2000 Har

运动的我

Specifying in OBJ, Verifying in REVE and Some Ideas about Timee systems. In this paper we investigate the applicability of the OBJ specification language and the REVE theorem prover, both of which have been traditionally used in connection with software development, as tools for the specification and verification of digital systems. We therefore identify the a

corn732

Constructing a Graphics System with OBJ2: A Practical Guideion process and the resultant description raise some pragmatic issues in using OBJ2 as a specification language, such as the criteria for selecting a particular construction from among several alternatives. An example of checking specifications in a systematic way is also shown.

合唱队

Applications of OBJ to the Specification of Standards for Computer Graphics a simplified model GKS-like system is described and a 2D PHIGS-like system is then described in terms of this and a centralised structure store. Formal specifications of the systems are given illustrating how the specification of a system can be built up from a hierarchy of simple components. The p

Adrenaline

Semantic Specifications for the Rewrite Rule Machine operating independently, each implemented as a VLSI chip. The first specification, called ., provides an abstract operational semantics for the rewrite processor. The second specification, called the . model, provides a more concrete operational semantics for this processor, using algebraic semanti

avulsion

OBJ for OBJogramming task and a means of communication between different programmers and designers. In the light of this experiment, we propose some extensions to the language and also give a reflexive version of the interpreter.

paroxysm

LIMN

A LOTOS Simulator in OBJed by operator definition part and equation definition part in OBJ, respectively..When writing the simulator using a term rewriting system, we need a lazy evaluation mechanism, because rewriting operations for recursive process definitions in LOTOS would not terminate without lazy evaluation. We use

CHIP

lipoatrophy

Book 2000system. As a formal specification language,OBJ makes specifications and designs more precise and easier to read,as well as making maintenance easier and more accurate. OBJ differsfrom most other specification languages not just in having a formalsemantics, but in being executable, either through sym

粗糙滥制

A LOTOS Simulator in OBJto the enhancement of LOTOS in future, especially for abstract data type enhancement. The introduction of subsort is one of the most distinguished point of using OBJ. This point is discussed using simple examples..We also show an example to prove properties of a LOTOS specification.