Specifying software requirements is an important, complicated and error prone task. It involves the collaboration of several people specifying requirements that are gathered through several stakeholders. During this p...Specifying software requirements is an important, complicated and error prone task. It involves the collaboration of several people specifying requirements that are gathered through several stakeholders. During this process, developers working in parallel introduce and make modifications to requirements until reaching a specification that satisfies the stakeholders’ requirements. Merge conflicts are inevitable when integrating the modifications made by different developers to a shared specification. Thus, detecting and resolving these conflicts is critical to ensure a consistent resulting specification. A conflicts detection approach for merging Object-Oriented formal specifications is proposed in this paper. Conflicts are classified, formally defined and detected based on the results of a proposed differencing algorithm. The proposed approach has been empirically evaluated, and the experimental results are discussed in this paper.展开更多
There is a growing tendency for people in the community of object-oriented methods to use preand post-conditions to write formal specifications for opera- tions （methods） of classes. The motivation for trying to tak...There is a growing tendency for people in the community of object-oriented methods to use preand post-conditions to write formal specifications for opera- tions （methods） of classes. The motivation for trying to take advantage of well established formalism in precisely defining the functionality of operations is laudable, but unfortunately this exercise may be flawed because the use of pre- and post-conditions containing method calls （or similar） with side effects are likely to cause confusion in the interpretation of specifications. This paper analyzes, with comprehensible examples, why using pre-post notation is not effective to specify operations in objectoriented systems in general, discusses existing approaches to using pre-post notation for object-oriented systems, and offers some solutions to the problem.展开更多
The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calc...The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.展开更多
文摘Specifying software requirements is an important, complicated and error prone task. It involves the collaboration of several people specifying requirements that are gathered through several stakeholders. During this process, developers working in parallel introduce and make modifications to requirements until reaching a specification that satisfies the stakeholders’ requirements. Merge conflicts are inevitable when integrating the modifications made by different developers to a shared specification. Thus, detecting and resolving these conflicts is critical to ensure a consistent resulting specification. A conflicts detection approach for merging Object-Oriented formal specifications is proposed in this paper. Conflicts are classified, formally defined and detected based on the results of a proposed differencing algorithm. The proposed approach has been empirically evaluated, and the experimental results are discussed in this paper.
文摘There is a growing tendency for people in the community of object-oriented methods to use preand post-conditions to write formal specifications for opera- tions （methods） of classes. The motivation for trying to take advantage of well established formalism in precisely defining the functionality of operations is laudable, but unfortunately this exercise may be flawed because the use of pre- and post-conditions containing method calls （or similar） with side effects are likely to cause confusion in the interpretation of specifications. This paper analyzes, with comprehensible examples, why using pre-post notation is not effective to specify operations in objectoriented systems in general, discusses existing approaches to using pre-post notation for object-oriented systems, and offers some solutions to the problem.
基金the National Natural Science Foundation of China (No.69673006) and theNational Ninth Five-Year Project (98-780-01-07-06) of Ch
文摘The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.
