一句话：为分布式 actor 程序提出契约语言并发展软验证技术，以在降低运行时契约检查开销的同时保留契约保障。
契约式设计要求程序员为程序元素标注契约规约，明确对使用方与实现方的期望，该实践已应用于高阶编程语言等场景，但分布式 actor 程序的契约支持仍然有限。与此同时，契约规约必须在程序运行时检查，会带来显著开销；已有的软验证技术可以验证部分契约规约，但仅在串行程序的语境中使用。因此本文的研究目标有两方面：为分布式 actor 程序设计契约语言，并为其开发软验证技术。文中给出了研究计划与方法，并展示了初步结果。
Design-by-contract is a software engineering practice where programmers annotate program elements with contract specifications that make expectations towards the user and supplier of the program element explicit. This practice has been applied in various contexts such as higher-order programming languages. However, support for contracts in distributed actor programs is limited. Unfortunately, contract specifications need to be checked while executing the program which introduces a substantial overhead. To counter this, soft verification techniques have been proposed to verify (parts of) contract specifications, but have only been applied in the context of sequential programs. The goal of our research is therefore twofold: designing contract languages for distributed actor programs and developing techniques for their soft verification. In this context, we present a work plan and method, and show our preliminary results.