A simple abstract model of Eiffel is introduced, and its denotational seman-tics is defined using VDM style. A static analysis approach is presented to treatmultiple inheritance and renaming mechanism. Within the fram...A simple abstract model of Eiffel is introduced, and its denotational seman-tics is defined using VDM style. A static analysis approach is presented to treatmultiple inheritance and renaming mechanism. Within the framework of deno-tational semantics iatroduced in this paper, the key features of Eiffel, such asidentification, classification, multiple inheritance, polymorphism and dynamicbinding, can be adequately characterized.展开更多
This paper describer the design and implementation of an experimental software automation system(NDAUTO).By combining the transformational and procedural approaches in software gutomation,the system can tansform softw...This paper describer the design and implementation of an experimental software automation system(NDAUTO).By combining the transformational and procedural approaches in software gutomation,the system can tansform software unctional specifications written in a graphical specification language GSPEC to executable programs sutomatically,The equivalence between a specification and its corresponding program can be guaranteed by the system,and the correctness of the specification can also be validated.The main new points of the work lie in the design of the specification languange,the transformation mechanism and the correctness validation of the specification.展开更多
Some computational issues on abduction are discussed in a framework of the first order sequent calculus. Starting from revising the meaning of 'good' abduction, a new criterion of abduction called intuitive-mi...Some computational issues on abduction are discussed in a framework of the first order sequent calculus. Starting from revising the meaning of 'good' abduction, a new criterion of abduction called intuitive-minimal abduction (IMA) is introduced.An IMA is an abductive formula equivalent to the minimal abductive formula under the theory part of a sequent and literally as simple as possible. Abduction algorithms are presented on the basis of a complete natural reduction system. An abductive formula, obtained by the algorithms presented in this papert is an IMA if the reduction tree, from which the abduction is performed, is fully expanded. Instead of using Skolem functions, a term-ordering is used to indicate dependency between terms.展开更多
文摘A simple abstract model of Eiffel is introduced, and its denotational seman-tics is defined using VDM style. A static analysis approach is presented to treatmultiple inheritance and renaming mechanism. Within the framework of deno-tational semantics iatroduced in this paper, the key features of Eiffel, such asidentification, classification, multiple inheritance, polymorphism and dynamicbinding, can be adequately characterized.
文摘This paper describer the design and implementation of an experimental software automation system(NDAUTO).By combining the transformational and procedural approaches in software gutomation,the system can tansform software unctional specifications written in a graphical specification language GSPEC to executable programs sutomatically,The equivalence between a specification and its corresponding program can be guaranteed by the system,and the correctness of the specification can also be validated.The main new points of the work lie in the design of the specification languange,the transformation mechanism and the correctness validation of the specification.
文摘Some computational issues on abduction are discussed in a framework of the first order sequent calculus. Starting from revising the meaning of 'good' abduction, a new criterion of abduction called intuitive-minimal abduction (IMA) is introduced.An IMA is an abductive formula equivalent to the minimal abductive formula under the theory part of a sequent and literally as simple as possible. Abduction algorithms are presented on the basis of a complete natural reduction system. An abductive formula, obtained by the algorithms presented in this papert is an IMA if the reduction tree, from which the abduction is performed, is fully expanded. Instead of using Skolem functions, a term-ordering is used to indicate dependency between terms.
