Theory: Algebraic and Logical Design Methods
Specification and programming
- Common algebraic specification language
- Data and processes
- Semantics online
- Hierarchical structure of systems
Accurate and unambiguous specification of software and hardware systems is a topic of major interest in the Logic and Computation group. Our research involves the development and use of algebraic specifications, as well as novel approaches to the semantics of programming languages.
Common algebraic specification language
A major achievement, involving a decade of research by the members of CoFI, the international Common Framework Initiative for algebraic specification and development, has been the creation of Casl, the Common Algebraic Specification Language. Casl is a general-purpose language for practical use in software development for specifying both requirements and design. It is already regarded as a de facto standard, and various sublanguages and extensions are available for specific tasks.
P D Mosses was overall coordinator of CoFI during the design of Casl, a co-author of the Casl User Manual, and the main editor of the Casl Reference Manual. As a member of CoFI, M Roggenbach was co-author of the standard library of Basic Datatypes in Casl, developed tools such as the consistency checker CCC for Casl, and
works on reactive language extensions for Casl.
Data and processes
Distributed computer applications such as flight booking systems, web services, or electronic payment systems, exhibit concurrent behaviour as well as data aspects. In order to model and analyse such systems, we design and test concurrent extensions of Casl, such as Co-Casl and CSP-Casl.
This requires foundational work on semantical questions as, e.g., if a process algebra can be formulated in the rather logical framework of an institution. As a major industrial case study in CSP-Casl, an electronic payment transaction standard is being specified and tested with H Schlingloff (Humbold University and Fraunhofer Institute, Berlin), the software house Zühlke (Zürich), and the company c.a.r.u.s. IT (Hamburg). Research on tool support for specification languages include the development CSP-Prover, an interactive theorem prover for the process algebra CSP, that is developed in close cooperation with Y Isobe (AIST, Japan). This research is supported by EPRSRC grant EP/D037212/1.
Semantics online
Since the middle of the last century, hundreds of programming languages have been designed and implemented – and new ones are continually emerging. The syntax of a programming language can usually be described quite precisely and efficiently using formal grammars. However, the formal description of its semantics is much more challenging. Language designers, implementers and programmers commonly regard precise semantic descriptions as impractical and too costly. Research in semantics has allowed us to reason about software and has provided valuable insight into the design of programming languages, but few semantic descriptions of full languages have been published, and hardly any of these are currently available online.
P D Mosses has developed two novel frameworks (Action Semantics and Modular Structural Operational Semantics) that allow the semantics of individual language constructs to be described independently, thus providing the basis for an online repository of reusable components for use in complete language descriptions.
Hierarchical structure of systems
N A Harman is trying to create a unified algebraic theory for computers from low-level hardware to high-level programs, using equational methods and tools for specification, simulation, and verification. Algebraic methods for modelling microprocessors at instruction set architecture (ISA) and microarchitecture levels of abstraction, and for proving their equivalence, have been developed and extended to pipelined and superscalar processors. These methods have been adapted for use in HOL verifications at Cambridge, where the first complete verification of a COT processor - the ARM - has been completed.
