运动的我
发表于 2025-3-25 05:25:34
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
发表于 2025-3-25 10:13:44
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.
合唱队
发表于 2025-3-25 14:51:10
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
发表于 2025-3-25 16:01:49
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
发表于 2025-3-25 21:41:21
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
发表于 2025-3-26 03:22:26
http://reply.papertrans.cn/88/8709/870878/870878_26.png
LIMN
发表于 2025-3-26 08:03:07
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
发表于 2025-3-26 09:26:32
http://reply.papertrans.cn/88/8709/870878/870878_28.png
lipoatrophy
发表于 2025-3-26 13:00:54
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
粗糙滥制
发表于 2025-3-26 18:46:08
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.