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.