What is a system supposed to do? The accurate and unambiguous specification of software and hardware systems is a massive problem. We pursue radical new approaches to the design and construction of programming and  specification languages.

Algebraic specification

Specification in the large allows us to model systems using components. Algebraic specification methods have provided a rich variety of operators that allow us to build complex specifications out of simpler ones. In the context of data, these structuring mechanisms with their relations to proof calculi have been studied extensively. Dr Markus Roggenbach applies these ideas to state based systems using the specification language CSP-CASL, developing proof calculi that exploit the specification structures to ease verification.

Process algebra, e.g. CSP, offers different semantical observations (e.g. traces, failures, divergences) on a single syntactical system description. These observations are either computed algebraically from the process syntax, or “extracted” from a single operational model. In co-operation with Professor Luis Monteiro (Lisbon), Dr Roggenbach studies bialgebraic semantics for CSP and CSP-CASL. Bialgebras capture both approaches in one framework and characterize their equivalence; however, due to use of finality, they lack the capability to simultaneously cater for various semantics. By relaxing finality to quasi-finality it is possible to study several semantics in parallel, which also can be coarser than bisimulation.

Programming language specification

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 be specified quite precisely and efficiently using formal grammars. However, to give a formal specification of its semantics is much more challenging. Research in semantics has allowed us to reason about software and has provided valuable insight into the design of programming languages, but language designers, implementers and programmers commonly regard precise semantic specifications as impractical and too costly.

Professor Peter Mosses has previously developed techniques for radically improving the practicality of language specification. He is now leading the PLanCompS research project, based at Swansea, Royal Holloway and City, funded by EPSRC, with Microsoft Research Cambridge as project partner. PLanCompS aims to establish and test the practicality of a component-based framework for the design, specification and implementation of programming languages. The main novelty will be the creation of a substantial collection of highly reusable, validated language components called fundamental constructs (funcons). Crucially, the semantic specification of each funcon will be independent, not needing any reformulation when funcons are combined or new funcons are added to the collection. All specifications will be provided online in an open access repository, with browsing and searching supported by a digital library interface.