第二屆 程式語言暨系統研討會



交通大學 資訊科學系 及

中央研究院 資訊科學研究所 合辦


民國八十六年十二月二十九日 ( 星期一 )



The 2nd Joint Seminar on Programming Languages and Systems



Dept. of Computer and Information Science, Chiao-Tung University

and

Institute of Information Science, Academia Sinica


December 29, Monday, 1997


Purposes


This seminar brings together researchers and students working on programming languages and systems to present results in their fields. It aims to provide a stimulating environment to further facilitate the exchange of ideas and experiences among the participants.


Schedule


9:20-9:30 am
曾憲雄 交通大學資訊科學系
Opening ceremony
9:30-10:20 am
項潔 臺灣大學資訊工程系 (Jieh Hsiang, National Taiwan University)
Order-Sorted Equational Specification and Completion
10:20-11:10 am
顏嗣鈞 臺灣大學電機工程系 (Hsu-Chun Yen, National Taiwan University)
Verification of Infinite-State Systems
11:10-12:00 am
黃廷祿 交通大學資訊工程系 (Ting-Lu Huang, National Chiao-Tung University)
Manual verification of concurrent programs using fetch_and_store primitives
1:30-2:20 pm
黃秋煌 東華大學 (Chua-Huang Huang, NDHU)
High-Performance Fortran: A Fortran Extension for Computational Science
2:20-3:10 pm
郭譽申 中央研究院資訊所 (Yue-Sun Kuo, Academia Sinica)
Non-Intrusive Object Intropsection in C++ -- Architecture and Application
3:10-4:00 pm
許秉瑜 中央大學企管系 (PingYu Hsu, National Central University)
Improving SQL with Generalized Quantifiers


Time and Place


The seminar will be held at 新竹市 交通大學 電機資訊大樓 七樓 on Decemer 29 (Monday), 1997. A map of NCTU is available at http://www.cis.nctu.edu.tw/~plas/gif/nctucampus.gif.

Students are especially welcomed to attend this seminar series. There is no registration fee for the seminars. Free lunches will be provided. To help plan the event, however, please send a plain-text e-mail to wuuyang@cis.nctu.edu.tw or fax to (03) 5721490 楊武 with your name (both in Chinese and English) and your current affiliation if you plan to attend. Further information about this event, including abstracts of the talks, will be available from WWW at http://www.cis.nctu.edu.tw/~plas/plas1997.html.

Campus accommodation is available. The cost is $600 per night per room (for a room with 2 beds). If you need to reserve a guest room, please send your order to wuuyang@cis.nctu.edu.tw. Since the room is on the first-come first-serve base, please reserve the room as early as possible.


Abstracts


項潔 Jieh Hsiang, National Taiwan University
Order-Sorted Equational Specification and Completion
顏嗣鈞 Hsu-Chun Yen, National Taiwan University
Verification of Infinite-State Systems

In this talk, we survey some of the recent results in the verification of infinite-state systems. In particular, we focus on the equivalence problem and the model checking problem. Given two infinite-state systems, the equivalence problem is to determine whether the two systems are `equivalent' with respect to a certain notion of equivalence. The model checking problem is that of deciding whether a given infinite-state system satisfies a formula in a certain temporal logic. The families of infinite-state systems addressed in this talk include Petri nets, pushdown automata, Basic Process Algebra, Basic Parallel Processes, and more.


黃廷祿 Ting-Lu Huang, National Chiao-Tung University
Manual verification of concurrent programs using fetch_and_store primitives

Concurrent programs can be very subtle and error-prone. The difficulty is due not to the size of the code, but to the intrinsic complexity of concurrency. Researchers continue to make serious mistakes in designing mutual exclusion algorithms even of the size less than 20 statements. The mistakes can be traced to poor understandings on the subtleties of either concurrent processes or the hardware primitives. Verification disciplines could have prevented such mistakes. In this talk, we will examine two particular small programs that use the fetch_and_store primitives. Both were published in recent IEEE periodicals but were later found incorrect by our group, one violating mutual exclusion and the other deadlock freedom. We will illustrate some verification techniques that are easy to apply manually. By showing what were done wrong and what could have been done right, we are reminded, once again, that manual verification on concurrent algorithms, with some reasonable level of rigor, is not as difficult as we usually perceive. And the benifit is clear: better understandings of one's own design.


黃秋煌 Chua-Huang Huang, National D.H. University
High-Performance Fortran: A Fortran Extension for Computational Science
郭譽申 Yue-Sun Kuo, Academia Sinica
Non-Intrusive Object Intropsection in C++ -- Architecture and Application

We describe the design and implementation of system architecture to support object introspection in C++. An introspective object permits observation and change to its own state by a general mechanism that is applicable to objects of all classes. This general mechanism allows the construction of applications where objects are late-binding and the interactions between them are highly dynamic.

Unlike Java, which provides full support for object introspection, C++ has limited built-in introspective capability via its Run-Time Type Information (RTTI) and related facilities. For example, in C++ one cannot query an object for methods that can be applied to it. We show how such introspective information can be collected at compile-time by parsing class declarations, and be used to build a supporting environment for object introspection at run-time.

Our approach is non-intrusive because it requires no change to the original class declarations and libraries, and it guarantees compatibility between objects before and after the addition of introspective capability. This is important if one wants to integrate third-party class libraries, which are often supplied as black boxes and allow no modification, into highly dynamic applications. We show two applications that are built on top of our introspective environment. The first is a generic facility for automatic I/O support of complex C++ objects. The other is a class exerciser that allows interactive execution of dynamically loaded C++ class libraries.

(Joint work with Tyng-Ruey Chuang and Chien-Min Wang)


許秉瑜 PingYu Hsu, National Central University
Improving SQL with Generalized Quantifiers

Generalized quantifiers are frequently-used phrases such as:

three, Chamberlin's three, more than three, fewer than three, at most three, exactly three, all but three, half, no more than three, not more than half, most but not all, at least two and not more than three, more than half but not all, neither Chamberlin's nor Astrahan's.

Since these quantifiers can be quite complex and are difficult to characterize, they are not treated explicitly by most query languages. Unfortunately, as shown in the introduction section, this lack of treatment forces users to write long and error-prone queries.

In this paper, we will show that a well-defined subset of quantifiers, reducible-to-safe quantifiers, can be implemented with operators supported by SQL2. Syntactic sugaring is then designed for these quantifiers to show they can be incorporated into SQL2 effectively, in a way that permits shorter, more natural queries.

We concentrate our discussion and implementation on SQL2, since it is the dominant query language, and most databases support some kind of SQL-like interface. However, our discussion also should be applicable to other query interfaces.