Past and ongoing research emphasizes rigorous methodology for the design, implementation and verification of implementation, of high level programming languages. This methodology is based on rigorous specification of criteria for the design of the language which are used to derive structural aspects of the language which ensure satisfaction of these criteria in the most natural way for human comprehension, while guaranteeing efficiency of implementation. Furthermore, these structural aspects should facilitate rigorous reasoning about programs written in the language. Obtaining language structures which simultaneously support these three main aims is important if the programming language is to permit cogent communication of algorithms and software systems in general between programmers in a manner which allows their efficient execution while at the same time facilitating their mathematical analysis. These goals conflict in general and obtaining language constructs satisfying them simultaneously is the subject of extensive international research at the present time and our own ongoing research.
Effective use of languages satisfying the kinds of criteria stated above require the representation of considerably more information and formal analysis tools than is required for earlier programming languages. Hence, they require environments which support such activities as:
Our ongoing research is concerned with the design and implementation of such environments which would enhance the rigour of the design, implementation and use high level specification and programming languages.
If you would like to examine how these ideas have been applied in a third year undergraduate software engineering course (1996, 1997) on the web click HERE!!!
Concurrent systems consisting of collections of simultaneously executing sequential subsystems capable of interaction at arbitrary points in system behaviours are much more difficult to conceptualize than sequential systems with global control. In addition to the meaning of each sequential subsystem the meaning of the possible interactions between subsystems must be understood which introduces additional complexity. A programming language for concurrent systems should be designed in a manner minimizing this complexity without sacrificing expressiveness of the language with respect to decomposition into parallel subcomponents. If a solution to a problem exhibits a certain degree of independence of sub-solutions, the language should permit the same degree of concurrency (execution independence) in some program. The added comlexity of conceptualization introduced by concurrent systems increases the need for rigour in the design, implementation and analysis of programming languages and programs developed in it which we expressed above for sequential programming languages. Ongoing research has resulted in the design of the COSY (Concurrent System) language and the development of a corresponding mathematical concurrency theory supporting well reasoned design of concurrent system strategies. Theorems of the theory allow formal verification of global behavioural properties (e.g. observance of capacity bounds, absence of (partial or total system deadlock, absence of starvation). Two prototypes of an integrated environment for COSY of the type described above for sequential systems have been developed. Research is continuing in the area of language design and support environment development for concurrent systems.
The three types of research activity characterized above have originated from our previous work in the formal semantics of programming languages and the formal verification of programs which constitute important subareas of theoretical computer science. In these areas we have collaborated in the development of the Vienna Definition Method used in the formal definition of a number of programming languages (most notably PL/I) and the Axiomatic Method of C.A.R. Hoare. Ongoing research has lead to the development of more language and automata theoretic formalisms for the statement of the semantics of concurrent systems based on the object oriented system paradigm which is the subject of intensive international research at the present time.
To attain maximal utility of semantical formalisms there is need to develop associated formal systems for reasoning about the semantics. Conventional formulations of logic are often inappropriate for reasoning about dynamic systems, and they are even less suited to reason about concurrent and distributed systems. Furthermore, computer support for such reasoning requires that such logics be efficiently implementable. Our work in formal semantics and verification of programs using the axiomatic method has culminated in an effort to develop and study unconventional logics (e.g. computational logic, modal logic, temporal logic, process logic) which are more suited to the tasks described above. Hence, this aspect of our research has moved into the areas often described as Artificial Intelligence and Fifth Generation Systems. In general we are looking for mathematical theory which will permit adequate representation of knowledge about (possibly concurrent) systems and rigorous reasoning on the basis of this knowledge in computer based environments.
|Name:||Peter Ernst Lauer|
|Telephone Number:||+1-905-525-9140 ext. 27039|