A logical framework to model software development by multiple agents following a common specification
Abstract
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).
Cite
@article{arxiv.2211.01341,
title = {A logical framework to model software development by multiple agents following a common specification},
author = {Georgios V. Pitsiladis and Petros S. Stefaneas},
journal= {arXiv preprint arXiv:2211.01341},
year = {2023}
}
Comments
15 pages (including bibliography). To be submitted to Logical Methods in Computer Science