Yoonsik Cheon
Gary T. Leavens
- ~ALENCAR, A. J. AND GOGUEN, J. A. 1991. OOZE: An object oriented Z environment. In ECOOP'91 ~Proceedings of the European Conference on Object~Oriented Programming. Lecture Notes in ~Computer Science, vol. 512. Springer-Verlag, New York, 180-199. Google Scholar
- ~AMERICA, r. 1991. Designing an object-oriented programming language with behavioral subtyp- ~ing. In Proceedings of Foundatwns of Object-Oriented Languages. Lecture Notes in Computer ~Science, vol. 489. Springer-Verlag, New York, 60 90. Google Scholar
- ~AMERICA, P. 1990. A parallel object-oriented language with inheritance and subtyping. In ~Proceedzngs of OOPSLA ECOOP'90. SIGPLAN Not. 25, 10 (Oct.), 161 168. Google Scholar
- ~BEAR, S. 1988. Structuring for the VDM specification language. In Proceedzngs of the 2nd ~VDM-Europe Symposium. Lecture Notes in Computer Science, vol. 328. Springer-Verlag, New ~York, 2-25. Google Scholar
- ~BRUCE, K. B. AND WEGNER, P. 1990. An algebraic model of subtype and inheritance. In ~Advances ~n Database Programming Languages. Addison-Wesley, Reading, Mass., 75-96, Google Scholar
- ~CARDELLI, L. AND WEGNER, P. 1985. On Understanding types, data abstraction and po}ymor- ~phism. ACM Comput. Surv. 17, 4 (Dec.), 471-522. Google Scholar
- ~CARRINGTON, D., DUKE, D., DUKE, R., KING, P., ROSE, G., AND SMITH, G. 1989. Object-Z. An ~object-oriented extension to Z. In Formal Descrzptzon Techniques (FORTE'89). North-Holland, ~Amsterdam, 281-296 Google Scholar
- ~CHEON, Y. 1991. Larch/Smalltalk: A specification language for Smalltalk Tech. Rep. TR ~#91-15, Dept. of Computer Science, Iowa State Univ., Ames, Iowa.Google Scholar
- ~CHEON, Y. AND LEAVENS, G. T. 1994. A gentile introduction to Larch/Smalltalk specification ~browsers. Tech. Rep. 94-01, Dept of Computer Science, Iowa State Univ., Ames, Iowa. ~Available by anonymous ftp from ftp.cs iastate.edu and by email from almanac~cs.iastate.edu.Google Scholar
- ~CHEON, Y. AND LEAVENS, G. T. 1993. A quick overview of Larch/C ++. Tech Rep 93-18, Dept. of ~Computer Science, Iowa State Univ, Ames, Iowa. Available by anonymous ftp from ftp.cs.ia- ~state edu and by email from almanac(~,cs.mstate.edu.Google Scholar
- ~CLERICI, S., AND OREJAS, F. GSBL: An algebraic specification language based on inheritance ~1988. In ECOOP'88, European Conference on Ob2ect-Orzented Programmtng. Lecture Notes in ~Computer Science, vol. 322. Sprmger-Verlag, New York, 78 92 Google Scholar
- ~COOK, W. R 1992. Interfaces and specifications for the SmalltaIk-80 collection classes. In ~Proceedings of OOPSLA '92. SIGPLAN Not. 27, 10 (Oct.), 1-15. Google Scholar
- ~COOK, W. R 1989. A proposal for making Eiffel type-safe. In ECOOP'89, European Conference ~on Object-Oriented Programmtng. Cambridge University Press, UK. 57 70.Google Scholar
- ~DAHL, O.-J. 1987 Object-oriented specifications. In Research Directions ~n Object-Oriented ~Programmzng. MIT Press, Cambridge, Mass., 561-576. Google Scholar
- ~ERNSqP, G. W., NAVLAKHA, J. K., AND OGDEN, W. F. 1982. Verification of programs with proce- ~dure-type parameters Acta Informatica 18, 2, 149-169.Google Scholar
- ~GOGUEN, J. A. AND MESEGUER, J. 1987. Order-sorted algebra solves the constructor-selector, ~multiple representation and coercion problems. In Symposium on Logic tn Computer Science. ~IEEE Computer Society Press, Los Alamitos, Calif., 18-29.Google Scholar
- ~GOLDBERG, A. AND ROBSON, D. 1983. Smalltalk-80. The Language and Its Implementatwn. ~Addison-Wesley, Reading, Mass. Google Scholar
- ~GUTTAG, J. V. AND HORNING, J. J 1993. Larch: Languages and Tools ~ir Formal Spectficatlon. ~Springer-Verlag, New York. Google Scholar
- ~GUTTAG, J. Y. AND HORNINO, J. J. 1991. Introduction to LCL, a Larch/C interface language. ~Tech. Rep. 74, Digital Equipment Corporation, Systems Research Center. Palo Alto, Calif.Google Scholar
- ~GUTTAG, J. V., HORNINC-, J. J., AND WINd, J. M. 1985. The Larch family of specification ~languages. IEEE Softw. 2, 4 (Sept).Google Scholar
- ~HAYES, I, El). 1987. Spectficatton Case Studles. International Series in Computer Science ~Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- ~HOARE, C. A. R. 1972. Proof of correctness of data representations Acta Informattca 1, 4, ~271 281.Google Scholar
- ~HOARE, C A. R. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 ~(Oct) 576-583. Google Scholar
- ~JONES, K. D. 1991. LM3: A Larch interface language for Modula-3, a definition and introduction ~version 1.0. Tech. Rep 72, Digital Equipment Corporation, Systems Research Center, Palo ~Alto, Calif.Google Scholar
- ~JUNGCLAUS, R., SAAKE, G., AND SERNADAS, C. 1991. Formal specification of object systems. In TAPSOFT'91 Proceedings of the International Joint Conference on Theory and Practice of ~Software Development. Lecture Notes m Computer Science, vol. 494. Springer-Verlag, New ~York, 60 82. Google Scholar
- ~LALoNI)E, W. R. 1989. Designing families of data types using examplars, ACM Trans Program ~Lang. Syst. 11, 2 (Apr.) 212-248. Google Scholar
- ~LALONDE, W. R., THOMAS, D. A., AND PUGH, J. R. 1986. An exemplar based Smalltalk. In ~Proceedings of the OOPSLA'86 Conference. SIGPLAN Not. 2J, 11 (Nov) 322-330. Google Scholar
- LEAVENS, G. T. 1993. Inheritance of interface specifications (extended abstract). Tech. Rep. 93-23, Dept. of Computer Science, Iowa State Univ. Ames, Iowa. Available by anonymous ftp from ftp.cs.iastate.edu or by email from [email protected].Google Scholar
- LEAVENS, G. T. 1991. Modular specification and verification of object-oriented programs. IEEE Softw. 8, 4 (July), 72-80. Google Scholar
- LEAVENS, G. T. AND CHEON, Y. 1992. Preliminary design of Larch/C ++. In Proceedings of the 1st International Workshop on Larch. Workshops in Computing Science, Springer-Verlag, New York. Google Scholar
- LEAVENS, G. T. AND WEIHL, W. E. 1990. Reasoning about object-oriented programs that use subtypes (extended abstract). In Proceedings of OOPSLA ECOOP'80. SIGPLAN Not. 25, 10 (Oct.), 212-223. Google Scholar
- LISKOV, B. AND WING, J. M. 1993a. A new definition of the subtype relation, in ECOOP'93-- Object-Oriented Programmtng. Lecture Notes in Computer Science, vol. 707. Springer-Verlag, New York, 118-141. Google Scholar
- LISKOV, B. AND WING, J. M. 1993b. Specifications and their use in defining subtypes. In Proceedings of OOPSLA'93 SIGPLAN Not. 28, 10 (Oct.), 16-28. Google Scholar
- MAYER, T. 1988. Specification of object-oriented systems in LOTOS. In Formal Descmption Techniques (FORTE'88). North-Holland, Amsterdam, 107-119. Google Scholar
- MEYER, B. 1988a. Eiffel: A language and environment for software engineering. J. Syst. Softw. 8, 3 (June), 199-246. Google Scholar
- MEYER, B. 1988b. Object-oriented Software Construction. International Series in Computer Science, Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- REYNOLDS, J. C. 1980. Using category theory to design implicit conversions and generic operators. In Proceedings of a Workshop on Semantics-Directed Compiler Generatton. Lecture Notes in Computer Science, vol. 94. Springer-Verlag, New York, 211-258. Google Scholar
- SCHAFFERT, C., COOPER, T., BULLIS, B., KILIAN, M., AND WILPOLT, C. 1986. An introduction to Trellis/Owl. In Proceedings of OOPSLA '86. SIGPLAN Not. 21, 11 (Nov.), 9-16. Google Scholar
- SCHUMAN, S. AND PITT, D. 1986. Object oriented subsystem specification. In Proceedzngs of the IFIP TC2 / WG 2.1 Working Conference on Program Specification and Transformation Program Specfftcation and Transformatzon. North Holland, Amsterdam, 313-342. Google Scholar
- TAN, Y. M. 1992. Semantic analysis of Larch interface specifications. In Proceedings of the 1st International Workshop on Larch. Workshops in Computing, Springer-Verlag, New York. Google Scholar
- WILLS, A. 1992. Specification in Fresco. in Object Ortentation in Z. Workshops in Computing, Springer-Verlag, Cambridge, UK, 127-135. Google Scholar
- WING, J. M. 1990. Using Larch to specify Avalon/C +~- objects. IEEE Trans. Softw. Eng. 16, 9 (Sept.), 1076-1088. Google Scholar
- WING, J. M. 1987. Writing Larch interface language specifications. ACM Trans. Program. Lang. Syst. 9, 1 (Jan.}, 1-24. Google Scholar
- WIN~, J. M. 1983. A two-tiered approach to specifying programs. Tech. Rep. TR-299, MIT, Lab. for Computer Science, Cambridge, Mass. Google Scholar
Index Terms
- The Larch/Smalltalk interface specification language
Recommendations
Writing Larch interface language specifications
Current research in specifications is emphasizing the practical use of formal specifications in program design. One way to encourage their use in practice is to provide specification languages that are accessible to both designers and programmers. With ...
Extending a Component Specification Language with Time
In a formal approach to component specification, interfaces are usually described using pre- and postconditions of methods or protocols. In this paper we present an approach for integrating time into a component specification language which already ...
A Formal Framework for ASTRAL Intralevel Proof Obligations
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Comments