论文标题
遵循共同规范的多个代理商对软件开发建模软件开发的逻辑框架
A logical framework to model software development by multiple agents following a common specification
论文作者
论文摘要
在本文中，我们通过多个不同的程序员（或编程团队）来解决程序的开发，每个程序员（或编程团队）都在不同的设置（编程语言或推理框架）中工作，但遵循共同的规范；特别是，我们在抽象的层面上研究了其生产程序之间的可翻译性问题。为此，在考虑了有关计划发展的一些哲学问题（包括其与科学理论化的相似性和差异）之后，我们扩展了一个逻辑框架，旨在描述相对主义者环境中的科学理论：我们的扩展增加了有关程序的推理能力，其一代过程的迭代过程及其规格。因此，我们能够在程序发生器的输出之间定义翻译概念，并证明当两个程序生成器可靠地遵循相同的规范（从特定的可靠性意义上）时，有一个（微不足道的）翻译。
In this paper, we address program development by multiple different programmers (or programming teams), each working in different settings (programming languages or reasoning frameworks), but following a common specification; in particular, we examine at an abstract level the problem of translatability between their produced programs. To this end, after consideration of some philosophical issues regarding program development, including its similarities and dissimilarities with scientific theorising, we extend a logical framework built to describe scientific theorising in relativist settings: our extensions add the ability of reasoning about programs, the iterative process of their generation, and their specifications. We are thus able to define a notion of translation between the outputs of program generators and prove that there is a (trivial) such translation when two program generators follow the same specification reliably (in a specific sense of reliability).
