在线验证的愿景-验证
A Vision for Online Verification-Validation
摘要：
今天的程序员面临着一个错误的选择，是创建可扩展的软件还是创建正确的软件。具体而言，动态语言允许软件具有丰富的可扩展性（通过动态代码加载、动态对象扩展和各种形式的反射），并且今天的程序员利用这种灵活性来“带来他们自己的语言特征”以丰富可扩展语言（例如，通过使用公共JavaScript库）。与此同时，这种基于库的语言扩展通常缺乏对其抽象的执行，导致难以避免和预测的编程错误。为了提供验证这个可扩展的世界，我们提出了在线验证验证（OVV），其中包括语言和VM设计，使一个“无阶段”的方法来程序分析，在对比标准的静态-动态阶段的区别。无阶段分析自由地将抽象解释与具体执行相结合，允许分析使用动态（具体）信息来证明关于未来执行的普遍（抽象）属性。在本文中，我们提出了一个概念概述OVV通过激励的例子程序，使用一个假设的数据库库。我们提出了一个通用的OVV语义，并扩展到这个语义，提供了一个简单的渐进的类型系统的数据库库原语。在OVV设置中实例化这个渐进类型系统的结果是一个检查器，它可以渐进地键入程序的连续延续，直到一个延续被完全验证。为了评估这个例子中OVV的建议愿景，我们实现了VM语义（在Rust中），并表明这种设计允许以这种方式进行渐进式类型化。
英文摘要：
Today's programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that is richly extensible (via dynamic code loading, dynamic object extension, and various forms of reflection), and today's programmers exploit this flexibility to "bring their own language features" to enrich extensible languages (e.g., by using common JavaScript libraries). Meanwhile, such library-based language extensions generally lack enforcement of their abstractions, leading to programming errors that are complex to avoid and predict. To offer verification for this extensible world, we propose online verification-validation (OVV), which consists of language and VM design that enables a "phaseless" approach to program analysis, in contrast to the standard static-dynamic phase distinction. Phaseless analysis freely interposes abstract interpretation with concrete execution, allowing analyses to use dynamic (concrete) information to prove universal (abstract) properties about future execution. In this paper, we present a conceptual overview of OVV through a motivating example program that uses a hypothetical database library. We present a generic semantics for OVV, and an extension to this semantics that offers a simple gradual type system for the database library primitives. The result of instantiating this gradual type system in an OVV setting is a checker that can progressively type successive continuations of the program until a continuation is fully verified. To evaluate the proposed vision of OVV for this example, we implement the VM semantics (in Rust), and show that this design permits progressive typing in this manner.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
