arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 1503.04918cs.LOcs.PL
收藏

Lucretia -脚本语言的交叉类型多态性

Lucretia - intersection type polymorphism for scripting languages

Marcin Benke, Viviana Bono, Aleksy Schubert

摘要:

从长远来看,脚本代码可能会带来维护问题。因此,需要一种方法,使以自动方式控制用动态语言编写的程序的属性成为可能。我们介绍了Lucretia,一种具有内省原语的核心语言。Lucretia配备了一个(改进的)静态类型系统,该系统基于描述所使用对象结构的类型的本地更新。通过这种方式,我们处理脚本语言最动态的特性之一,即对象接口的运行时修改。在我们的系统中,判断有一个类似霍尔的形状,因为它们有一个先决条件和一个后置条件部分。前置条件描述了在某个表达式执行之前可见对象的接口的静态近似,后置条件描述了表达式执行之后的接口。字段更新操作使系统中的混叠问题复杂化。我们通过在方法签名中引入交集类型来应对它。

英文摘要:

Scripting code may present maintenance problems in the long run. There is, then, the call for methodologies that make it possible to control the properties of programs written in dynamic languages in an automatic fashion. We introduce Lucretia, a core language with an introspection primitive. Lucretia is equipped with a (retrofitted) static type system based on local updates of types that describe the structure of objects being used. In this way, we deal with one of the most dynamic features of scripting languages, that is, the runtime modification of object interfaces. Judgements in our systems have a Hoare-like shape, as they have a precondition and a postcondition part. Preconditions describe static approximations of the interfaces of visible objects before a certain expression has been executed and postconditions describe them after its execution. The field update operation complicates the issue of aliasing in the system. We cope with it by introducing intersection types in method signatures.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑