用于大规模可验证安全流网络增量与模块化设计的领域特定语言（初步报告）
编程语言
2011-09-06 v1 分布式、并行与集群计算
计算机科学中的逻辑
软件工程
摘要
我们定义了一种领域特定语言 (DSL)，用于从小型网络或模块归纳地组装流网络，以生成任意大规模的网络，并具有可互换的功能等效部件。在我们的归纳定义中，小型网络或模块仅在作为构建块意义上是“小”的（对其大小没有限制）。与该 DSL 相关联的是一种类型论，这是一套形式化标注系统，用于表达流网络的理想属性，并通过规则将这些属性作为接口上的不变量强制执行，即规则保证在从小型网络构建大型网络时属性得以保持。类型论的前提是形式语义，即对符合通过网络可行流的实体进行严格定义，可能限制以满足额外的效率或安全要求。这可以通过两种方式之一进行：指称语义或操作（或归约）语义；我们选择前者而非后者，部分原因是为了避免操作方法中的指数级增长重写。我们建立了一个类型系统并证明了其对于该 DSL 的可靠性。
引用
@article{arxiv.1109.0775,
title = {A Domain-Specific Language for Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks (Preliminary Report)},
author = {Azer Bestavros and Assaf Kfoury},
journal= {arXiv preprint arXiv:1109.0775},
year = {2011}
}
备注
In Proceedings DSL 2011, arXiv:1109.0323