Abstract:JOOSL is an object-oriented formal specification language, which can be used to describe requirement specification, preliminary design and detailed design of an object-oriented software. From the view point of specification method, requirement specification is about the same as priliminary design. In these specifications the data and operations should be described abstractly. The detailed design is concerned with specifying algorithmic details and concrete data representations. In JOOSL, an object is considered as an abstract state machine and inheritance is defined as sharing of behavior.

Abstract:This paper introduces a method of automatically generating curve outline based Hu-Po character, which is on the basis of Yuan-Tou character features, using over-lapping rules.

Abstract:One of the advantages of XYZ/E is that both high level and low level specifications can be represented in the same frame work, so that it makes specification and implementation of software systems easier. It is important to develop verification tools to verify whether the expected relation between different levels of specifications holds. Rules for verification of XYZ/SE programs had been studied by Xie Hongliang et al. in a previous paper. This paper extends the set of the rules to include rules for use of arrays, for procedure specification and for procedure call. It puts the emphasis on the practical and mechanical aspects of the verification of XYZ/SE programs. A set of rules for simplifying verification conditions is also implemented.

Abstract:After brief discussion of communication software development based on STREAMS mechanism, the design and implementation of X. 25 accessing software based on STREAMS mechanism is presented, with which millions of microcomputer users can cornmunicate each other remotely.

Abstract:This paper gives the semantic synthesis rules for HOS's primitive structures J()IN INCLUDE .OR and co-structures COINCLUDE .COOR COJOIN. Based on these semantic rules, a hierarchical understanding method for HOS specification is presented and its applications to the verification and reuse of HOS specification are also discussed.

Abstract:In this paper, the modal resolution method presented by P. Enjalbert and L.Farinas del Cerro is extended to modal systems K₄ and D₄. Then, the soundness and completeness of R K₄ relative to K₄ is proved, and also for R D₄ relative to D₄.

Abstract:Proof of the initialization theorem is a standard check that may be carried out for any state-based specification. A procedure for proving initialization theorems is presented. The proof justifications can be generated automatically by this procedure. By way of example, two initialization theorems are proved using this procedure.