| EPSRC Reference: |
GR/J11058/01 |
| Title: |
A DEVELOPMENT METHOD FOR CONCURRENT (OBJECT-BASED) PROGRAMS |
| Principal Investigator: |
Jones, Professor CB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Victoria University of Manchester, The |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
17 December 1993 |
Ends: |
16 June 1997 |
Value (£): |
117,878
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To provide development methods for concurrent programs which approach as nearly as possible the usability of methods like VDM which have been used for sequential programs. Specifically, the original proposal foresaw the use of features of object-oriented programming languages in order to control the interference and put the decisions about granularity in the hands of the developer. Progress:The progress in this period has been along two main fronts and has achieved considerable results in both areas. Work on further developments of rely/guarantee conditions as a way of recording in specifications - and reasoning in developments about interference has progressed since the appointment of Dr. Pierre Collette on 1st August 1994.Dr. Collette and Professor Jones are currently co-operating on a paper which should be published during 1995. The main progress here has been methodological in the sense that we have been seeking recommendations which would make the existing rules known for handling rely/guarantee conditions acceptable to a wider range of developer skills. Related to this topic (although not directly on rely/guarantee conditions) is the thesis submitted in August 1994 by Dr. Carlos Camarao de Fugueiredo. This investigates the form of proof rules which are needed for sequential object-oriented program development and the intention is to use sequential design initially followed by transformational introduction of concurrency as a way of minimising the need to reason about the more cumbersome rely/guarantee conditions.Work on the POBL design language has progressed in collaboration with Mr. S. Hodges (an SERC funded post-graduate student) and Mr. Haruo Yamaguchi (a self-funded Japanese post-graduate student). We have jointly been developing both the POBL language itself and refining the presentation of its semantics. New applications of POBL are being investigated in order to check its expressiveness. Difficulties with proving the theorems which were needed in terms of the original pi-calculus semantics are slowly being overcome, partly by gaining extra intuitions from less formal reasoning about operational semantics descriptions of POBL. The work on POBL semantics should receive considerable further support by the arrival in 1995 of Dr. Kohei Honda who is a EPSRC funded Visiting Fellow.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
|