Reasoning About Low-Level Programming

建议对以提供存储和其他资源的低级视图的语言编写的计算机程序的规范和验证进行研究。这项研究将集中于两种特别关键的编程技术的新的形式化方法：共享可变数据结构-使用可能包含一个以上指向可由程序更新的位置的指针的表示。这些数据表示将在谓词逻辑的扩展中指定，称为分离逻辑，其中断言的结构反映了存储到分离组件的分离。嵌入式代码指针-使用数据表示法包含指向程序指令的可更新组件。使用代码指针的程序将通过使用允许代码出现在断言中的反射操作符来指定。要研究的低级编程的特定方面包括存储分配、共享变量并发以及规范和TYE系统之间的关系。作为这项研究的结果，将变得更容易避免在重要的有用但困难的计算机程序类别中出现错误。最终，应该可以使逻辑自动化，以便这个类中的程序可以伴随着机器可检查的正确性证明

Research is proposed on the specification and verification of computer programs written in languages that provide a low-level view of storage and other resources. This research will focus on novel formal methods for two particularly crucial programming techniques:Shared mutable data structure - the use of representations that may contain more than one pointer to a location that can be updated by the program. These data representations will be specified in an extension of predicate logic, called separation logic, in which the structure of assertions mirrors the separation of storage intoDisjoint components. Embedded code pointers - the use of data representationsContaining updatable components that point to program instructions. Programs using code pointers will be specified by using a reflectionOperator that allows code to occur within assertions.Specific aspects of low-level programming to be investigated includestorage allocation, share-variable concurrency, and the relationbetween specifications and tye systems.As a consequence of this research, it will become easier to avoiderrors in an important class of useful but difficult computer programs. Eventually, it should be possible to automate the logic so that programs in thisClass can be accompanied by machine-checkable proofs of their correctness