Relational and Algebraic Methods in Software Developement

*我们都经历过软件产品中的错误或bug。导致某些文本处理软件故障的错误可能非常烦人，但通常不会造成严重后果。另一方面，如果系统中的错误影响到安全关键系统，如飞机的自动驾驶仪或核电站的控制单元，故障是不可接受的。软件工程师通常开发良好的测试策略，使他们能够检测隐藏在程序中的大多数错误，但测试永远不能保证程序没有错误。形式方法是研究和应用基于数学的技术来解决这个问题。它们用于软件和硬件组件的规范、开发和验证。这通常是通过在执行特定代码之前提供一个应该满足的条件，在执行代码之后提供另一个将保持的条件以及对这一事实的证明来实现的。验证过程通常很复杂，而且非常耗时，因此经常使用（半）自动化定理证明器来自动化至少部分任务。从EAL5级开始，遵循信息技术安全评估通用标准（ISO/IEC 15408）的计算机系统认证需要使用（半）正式工具，这一事实表明了形式化方法的重要性。大多数形式方法都是基于一阶逻辑的语言和演算，即使用标准的逻辑运算和量词。另一方面，最近的实验表明，某些定理证明在代数理论中非常成功，也就是说，在公理和定理是方程的情况下，证明是类似于常规代数中的计算。本研究将二元关系的等式理论应用于程序的规范、开发和验证，主要集中在三个方面。首先，本研究将把二元关系的数学理论和微积分扩展到目前尚未开发出这种并行规划的领域。其次，将为交互式编程语言和定理证明者Coq开发一个包含关系理论及其实现的所有方面的库。由于Coq也是一种编程语言，我们将能够在一个系统中处理理论，证明和实现。该库将是理论的所有实际应用的基础，即任何经过验证的软件的具体开发。最后但并非最不重要的是，这些方面和工具将被应用于开发正确的软件，从概念示例到现实世界的应用。

*We have all experienced errors or bugs in software products. An error causing some text processing software to malfunction can be very annoying but it is normally not critical with serious consequences. On the other hand, if an error in a system affects a safety critical system such as the autopilot of an airplane or the control unit of a nuclear plant, failure is not acceptable. Software engineers usually develop good testing strategies allowing them to detect most errors hidden in programs, but testing can never guarantee that the program is free of errors. Formal methods are the study and application of mathematically-based techniques addressing this problem. They are used for the specification, development, and verification of software and hardware components. This is normally done by providing a condition that should be satisfied before executing a particular piece of code, another condition that will hold after executing the code and a proof of this fact. The verification process is usually complicated and very time consuming so that quite often (semi)automatic theorem provers are used in order to automate at least parts of the task. The importance of Formal Methods is indicated by the fact that a certification of a computer system following the Common Criteria for Information Technology Security Evaluation standard (ISO/IEC 15408) starting at level EAL5 requires the use of (semi)formal tools. Most approaches to formal methods are based on languages and calculi derived from first-order logic, i.e., they use the standard logical operations and quantifiers. On the other hand, recent experiments have shown that certain theorem provers work very successfully with algebraic theories, i.e., in situations where axioms and theorems are equations and proofs are calculations similar to those in regular algebra. This research will use the equational theory of binary relations in program specification, development, and verification by focusing on three major aspects. Firstly, the research will expand the mathematical theory and the calculus of binary relations into areas currently not yet developed such a parallel programming. Secondly, a library containing all aspects of the theory of relations and their implementation will be developed for the interactive programming language and theorem prover Coq. Since Coq is also a programming language we will be able to handle theory, proofs and implementation in one system. The library will be a base for all practical applications of the theory, i.e., any concrete development of verified software. Last but not least, these aspects and tools will be applied in order to develop correct software ranging from conceptual examples to real world applications.