Correct translation of abstract specifications to C-Code

抽象规范到C代码的正确翻译（VeriCode）基于精化的方法是开发验证软件的成功技术。 它通常以命令程序（组织在组件中）以及谓词逻辑中的数据结构和函数的公理化描述结束。许多项目成功地使用了这种方法。一个非常广泛的项目是我们的Flashix项目，在这个项目中，我们开发并验证了一个用于Flash存储器的文件系统。规范和程序使用谓词逻辑的引用透明复制语义，顺序程序的最弱前提演算，以及并发程序的可靠保证演算。 为了从这样的程序中得到可执行代码，定理证明器通常生成具有不可变数据结构的函数式程序。生成的代码通常是低效的，因为破坏性的更新（例如有效使用数组所必需的）通常是不正确的。 此外，对于操作系统内核中的应用程序或非实时应用程序，不可能进行必要的垃圾收集。这些都需要明确管理内存的代码，例如C-Code。从抽象的，引用透明的数据结构转移到高效的，破坏性的代码是困难的，因为明确的信息应该分配内存或更新可以覆盖不存在。在以前的工作中，我们已经开发了一种方法，以保持所有数据结构不相交的方式转换（非共享）组件之间，并修改非共享的数据结构破坏性。虽然这导致了相当大的改进，但与手动编写的代码相比，它仍然是低效的（ca。系数10，取决于应用），因为赋值x：= y仍然必须复制存储在y中的数据结构，包括所有子结构（如果y仍然被使用）。 这些复制操作通常可以通过仔细的分析来避免。这个项目的目标是开发一个系统的数据流分析，允许用最少的复制操作生成最佳的C代码，这样生成的代码比手动编写的代码更高效（因子1-3）。 为此，我们希望定义一个规范框架，其中包含抽象数据类型的代数规范，以及并发命令式程序。 我们希望正式指定数据流分析的核心，并验证从规范语言转换产生正确的代码，没有内存泄漏。为了证明项目的成功，其结果将通过几个案例研究进行评估。抽象规范框架允许项目结果被所有其他验证系统使用，并可以显着提高验证程序的实际使用。

Correct translation of abstract specifications to C-Code (VeriCode)The refinement based approach is a successful technique for the development of verified software. It usually ends with imperativeprograms (organized in components) together with axiomatic descriptions of data structures and functions in predicate logic. Many projects have used this methodology successfully. One very extensive project is our Flashix project, in which we developed and verified a file system for Flash memory.Specifications and programs use the referentially transparent copy semantics of predicate logic, the weakest precondition calculus forsequential programs, and a rely-guarantee calculus for concurrent programs. To get executable code from such programs, theorem provers typically generate functional programs with immutable data structures.The resulting code is usually inefficient since destructive updates, that are necessary for the efficient use of e.g. arrays, are notcorrect in general. In addition, the necessary garbage collection is not possible for applications in operating system kernels, or inreal-time applications. These require code that manages memory explicitly, e.g. C-Code.Moving from abstract, referentially transparent data structures to efficient, destructive code is difficult, since explicit informationwhere memory should be allocated or which updates can overwrite is not present.In previous work we have developed an approach, that translates in a way that keeps all data structures disjoint (unshared) betweencomponents, and modifies unshared data structures destructively. Although this leads to a considerable improvement it is stillinefficient compared to manually written code (ca. a factor of 10, depending on the application), since an assignment x := ystill has to copy the data structure stored in y including all substructures (if y is still used). These copy operations can often be avoided using a careful analysis.The goal of this project is to develop a systematic data flow analysis that allows the generation of optimal C-Code with a minimum of copy operations, such that the resulting code is comparably efficient to manually written code (factor 1-3). For this, we want to define a specification framework with algebraic specifications for abstract data types, as well as concurrent imperative programs. We want to formally specify the core of the data flow analysis and verify that the transformation from the specification language yields correct code without memory leaks.To document the success of the project, its results will be evaluated with several case studies.The abstract specification framework allows the project result to be used by all other verification systems, and can significantly improve the practical usage of verified programs.