Tool support for relational formalisms in programming and specification

点击翻译按钮获取中文摘要

The goal of this research is to improve software developers' productivity and confidence in their products by expanding the use of relational abstractions in different stages of software development.  It is well-known that in many application areas, in particular where networks of any kind are involved, concise relation-algebraic specifications are available for many tasks.  This research will open up new ways to make many of these specifications executable, with efficient, automatically tuned implementations.  In addition, similar formulations can be used in a wide range of applications, including "fuzzy" decision finding, configuration changes via graph transformations, and communication protocols.  This research will build a unified framework of tool support for specifying, programming, and reasoning in this family of languages.  It will study both stand-alone relation-based specification and programming, and embedding in functional programming, as well as new foundations for functional-logic programming.The unified approach to programming and specification taken by this research will open up more efficient ways of software development, in particular in the increasingly many application areas where software is used in safety-critical environments, and therefore must be certified as correct.Several strands of the more foundational aspects of this research will be used together to enable, as a practical application, generation of high-performance code to be used in medical imaging.  In this project, the theoretical foundations of this research will aid in constructing also the proofs that the generated medical imaging software satisfies its mathematical specifications, stated in the language of signal processing.