# A logical framework to model software development by multiple agents
following a common specification

Georgios V. Pitsiladis0000-0003-2279-7738  and  Petros S.
Stefaneas0000-0002-2096-9914  School of Applied Mathematical and Physical
Science, National Technical University of Athens, Greece
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### 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).

###### Key words and phrases:

logic of software development, programs, specifications, translatability,
methodology of software development, possible worlds, program generators

The first author has been funded by the Special Account for Research Funding
(E.L.K.E.) of the National Technical University of Athens. The second author
has been supported by the PEVE2021 action of the Special Account for Research
Funding (E.L.K.E.) of the National Technical University of Athens. This work
is dedicated to the late Aristidis Arageorgis

##  1\. Introduction

In [Ara17], A. Arageorgis, building on the work of [KJG92], constructs a
formal framework describing scientific theorising in the presence of many
variants of relativism: truth, meaning, logical framework, and evidence are
expected to depend on the actions, conjectures, and conceptual choices of each
scientist (or research programme) at any given time. Arageorgis proves that,
if two scientists (or research programmes) start with common background
knowledge and work in a way that asymptotically brings each of them close to
their respective truth about the world, then there will asymptotically be a
(trivial) translation between their resulting theories.

It has been argued [APT21] that software development has an empirical
character, albeit with some important differences compared to the empirical
character of natural science. Moreover, computer systems can be considered as
technical artefacts [Tur18]; in that sense, they require the use of some
background scientific knowledge in order to be built [AB89]. Both these
considerations lead us to believe that the framework defined in [Ara17] can be
(carefully) modified to reason fruitfully about program development; in
particular, given its translatability result and, more generally, its strength
in modelling situations where multiple agents work independently but share
some background assumptions, we feel that it can shed some light on similar
concerns in computer science.

With the above in mind, we extend the framework of [Ara17] to describe
software development. We reinterpret scientists (or research programmes) as
software developers (or teams). The notions of relativised truth, meaning,
logical framework, and evidence remain present in our generalisation. We add
that each developer (or team) produces a piece of code (a technical artefact)
at every time instant; hence, the relativised setting is extended with program
semantics, allowing different programmers to work in different programming
languages, or even programming paradigms, resulting in different program
semantics.

It is then possible to define a notion of translatability between the outputs
of program generators. As in [Ara17], we manage to obtain a proof that if two
programmers (or teams) start with common specification and work in a way that
asymptotically makes each one write correct programs relative to their shared
specification, then, there will asymptotically be a (trivial) translation
between their resulting programs and theories.

The rest of the paper is organised as follows: Section 2 contains
philosophical discussion on the ontology of programs and specifications and on
the methodology of software development; the purpose of this discussion is
threefold: (a) to argue on the feasibility of porting results form the
philosophy of natural science to reason about computer science, (b) to support
the conceptual choices made while adapting [Ara17] and developing our
framework, and (c) to provide an overview of the aspects of the development of
computational systems, especially in relation to programs and specifications,
from which the aspects that can or cannot be handled by our framework can be
inferred. Section 3 contains a detailed presentation of our framework.
Finally, Section 4 contains some concluding remarks.

##  2\. Philosophical considerations on program development

The development of computational systems has been characterised as an
empirical discipline [APT21, Section 8.3] and parallels can be drawn between
(parts of) its methodology and elements of the scientific method [Ang14]. This
is due to the need for verifying whether programs adhere to their
specification —a need that quickly becomes all the more urgent as programs
become more complex—, which is pursued by forming (maybe formal) theories of
the behaviour of the program and by observing executions of the program with
carefully selected input; both these aspects bear resemblances with scientific
theorising and experimentation.

Moreover, as noted by [Ang14], creating complete computational systems
definitely requires solving several problems pertaining to an array of
scientific disciplines: it is a _scientifically attested technology_ in the
sense of [AB89].

However, arguably, the analogy between software engineering and experimental
science has a number of peculiarities; [APT21] mentions some of them, the most
important being the difference between specifications and scientific theories
that we discuss in Section 2.3 below.

Thus, adapting the framework of [Ara17], designed for the description of
scientific theorising in the “hard sciences”, to obtain a framework that
describes program development might be sensible, but, in any case, it must be
carried out with care, in order to accommodate the differences between the two
kinds of disciplines.

Our treatment of software development will be based on a computer science
perspective, which, as argued by [Gru11], is different from (although related
to) a software engineering perspective. For example, we will ignore aspects of
software such as its cost, legal considerations (at least those not directly
expressed in the specification), and project management, i.e., those aspects
termed the _socio-technical modality_ by [DMP18]. We will also ignore
aesthetic qualities of programs, such as form and legibility; moreover, we
will not be concerned with simplicity (although, according to [Tur18, Section
2.3], it contributes to correctness).

###  2.1. Levels of abstraction

In [Pri16], building on the method of abstraction [Flo16], the basic levels of
abstraction (LoAs) in work when creating computational systems are identified
and discussed. They range from structured physical data (for example, bits
stored in a hard drive) to intentional information content (this corresponds
to _intention_ of [Tur20] or, maybe more loosely, to _requirements_ of [ZJ97];
for example, what kind of actions a travel agent expects a booking platform to
perform).

A full account of development of computational systems as complete entities
should take into account all the LoAs that are employed when building such
systems. In this work, we will not explore the full LoA hierarchy; for
example, we will not consider the actual circuits running a program (also
known as the _physical modality_ of [DMP18]). We will focus on programs and on
their specifications; in this context, a program is instructional information
in some programming language, while a specification is abstract (but still
formal) information which is meant to capture the intention of the
computational system stakeholders.

As stressed by [Flo16], LoAs require an analysis exhibiting _relationism_ :
pluralistic but without endorsing relativism. One of the goals of our work is
to express situations where two programmers (or programming teams) share a
part of the LoA hierarchy (in particular, they share a common specification)
but might be working with different elements in the lower LoAs, hence we
introduce a kind of “horizontal” relationism among the different agents, in
addition to the “vertical” relationism among the LoAs mentioned above. The
framework of [Ara17] seems fitting for that goal, since it was specifically
designed for a pluralistic analysis.

###  2.2. Programs: syntax and semantics

Programs are (sequences of) instructions given in some programming language.
As such, they are expressed as strings in some well-defined alphabet and they
must conform to the (formal) syntactic rules of their language.

In [Pri16], it is stressed that programs have no alethic values: their meaning
ultimately lies on their ability to control the operation of the physical
components of a machine, although this is mediated by the (abstract) semantics
of the programming language. Similarly, there are two main ways to study the
semantics of programming languages and programs: operational semantics, which
focuses on how each step of the program operates, and denotational semantics,
which focuses on the program as a whole; for a comparison and other notions of
semantics, see [Tur18].

While not having alethic values themselves, programs, being technical
artefacts, have both functional and structural properties [AP18, Section 3]:
in short, functional properties describe _what functionalities_ a program
implements, while structural properties describe _how_ it operates. Reasoning
on such properties is therefore possible, for descriptive or for normative
purposes. When programs are too complex, reasoning on their functional
properties might be accomplished by constructing models to act as their
proxies, in order to abstract away some of the complexity [Tur11, Section
_Model Construction_].

###  2.3. Specifications and verification

Specifications111As discussed in [AP18, Section 6.1], there are two notions of
“specifications” in the literature: _property_ specifications (called
_functional_ specifications in [Tur11]) and _system_ specifications. The
former describe what functional properties a program _should_ have, while the
latter describe what properties an _already constructed_ program has. The
notion of “specifications” in this paper refers to the first kind. define how
a program should function: they describe the functional properties that
produced programs should possess. Their articulation ranges from natural
language to specialised formal languages. Similarly (but not necessarily in
parallel), their level of detail and their level of formality can vary.

What is common to all specifications is their relation to programs: they form
a _dominant/submissive_ pair, in the sense of [Tur20]. In the words of
[Tur11], “it is the act of taking a definition to have normative force over
the construction of an artefact that turns a mere definition into a
specification”, or, more plainly, “something is a specification when it is
given correctness jurisdiction over an artefact”. This characteristic does not
stem from the form or the extensional content of the specifications, but from
the intention of their use as such [Tur20].

This is a key difference between specifications and scientific theories. While
it is in general true that specifications describe programs and scientific
theories describe the world, they “describe” in different senses. The latter
have explanatory and predictive character, while the former are normative (any
predictive or explanatory characteristics a specification might have are
incidental [Tur11, Section  _Specification and Theory_]). Accordingly, when
there is a mismatch between a scientific theory and the world, then the theory
must be revised; on the contrary, when there is a mismatch between a
specification and a program, then the program must be revised.

Notice that, as stressed by [Tur11], the relationship between programs and
their specifications is more complicated in practice. On the one hand,
specifications are not always correct themselves or may even be unrealistic;
these and other reasons imply that there are cases where a
program/specification misalignment causes the specification to be revised
instead of the program. On the other hand, especially in big systems, where
different parts of the specification have different degrees of importance, a
program might be accepted if it is “fit for use”, in the sense that it matches
the specification enough to be used for its (main) intended purpose, but not
(necessarily) completely. We will not tackle these considerations here, but we
will hint on how we believe they could be tackled.

Since specifications are truth-determining for programs (and, dually, programs
are correct in view of specifications), there arises the problem of checking
whether the created program has the intended properties: the problem of
verification. Verification of some sort, formal (theorem proving, model
checking), experimental (testing), or mixed is crucial in the development
process. In fact, [Ang20] argues that formal and experimental verification are
intertwined.

Often, when verifying that a program meets its specification, possible
failures in lower LoAs are tacitly or explicitly ignored [Ang13, Section
_Fairness Constraints as Ceteris Paribus Modifiers_][Tur20, Section
_Verifying Programs_]. Since we are focusing on the LoAs of programs and
specifications, our framework can be considered to incorporate such
simplifications in its design.

##  3\. A logic of software development

Fix a finite alphabet and let $S$ be the set of all strings that may be
written with characters of the alphabet; of course, $S$ is countably infinite.
Let $\mathtt{e}\in S$ be the empty string.

If $f\colon A\rightarrow B$ and $g\colon B\rightarrow C$ are functions, then
$f\mathbin{;}g$ is their composition.

$\omega$ is the set of natural numbers with their usual order. For a set $X$,
$X^{\omega^{\star}}$ is the set of all finite sequences of $X$; we accept that
$\emptyset\in X^{\omega^{\star}}$ by convention.

Let $\mathbf{P_{n}}$ be a predicate that depends on a parameter $n\in\omega$.
We can then form the predicate “$\mathbf{P_{n}}$ in the limit”,

$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\mathbf{P_{n}}\equiv\text{there
exists some }n\in\omega\text{ such that }m\geq n\text{ implies
}\mathbf{P_{m}}.$

######  Remark 1.

Let $\mathbf{P_{n}}$, $\mathbf{Q_{n}}$ be predicates. Then,
$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\left(\mathbf{P_{n}}\wedge\mathbf{Q_{n}}\right)$
iff $\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\mathbf{P_{n}}$
and
$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\mathbf{Q_{n}}$.

In the original framework of [Ara17], the objective part of truth and meaning
is modelled via possible worlds, a collection of which constitutes background
knowledge; at each stage of scientific inquiry, hypotheses generators (i.e.,
scientists or research programmes), after examining previous evidence given to
them by the world, output a hypothesis (i.e., a conjecture based on their
conceptual choices) and an action, to which each possible world responds with
fresh evidence and with a valuation of what they can consider true, false, or
meaningless based on their selected logical framework. Notions of language and
theory are defined on top of this interaction for every stage of inquiry.
Using these elements, some properties are stated that aim to express the
correctness and completeness of theories. Also, a notion of translatability
between theories is defined.

The notions of hypotheses, and actions, valuations, and evidence —and hence
also reasoning languages and theories—remain present in our generalisation,
since program generators (i.e., programmers, programming teams, or even
automatic code generators) entertain some hypotheses regarding the behaviour
of their produced code and its (natural as well as artificial) environment. We
add some code is produced at every time instant; hence, the response of the
possible worlds needs to be extended with program semantics, allowing
different programmers to work in different programming languages, or even
programming paradigms. The notion of background knowledge is reinterpreted to
model specifications regarding the deliverable piece of code. Moreover, we
state some properties that aim to express the well-formedness of a program and
its correctness relative to its specification. We also extend the notion of
translatability so as to include programs.

###  3.1. Programs

Let $P$ denote all possible programs; notice that $P$ may be allowed to not
contain only valid programs, but also any code that might be produced by
programmers (for example, code with typos). Since programs are actually
strings, it is enough to define $P\subset S$ for this presentation; however,
notice that programs could have more structure than just plain strings ($P$
could, for example, include structured metadata along with the code of each
program). We will need $P$ to contain an empty program; we will use the empty
string for that purpose, i.e., $\mathtt{e}\in P$.

Regarding the semantics of programs, we do not want to restrain ourselves to
some particular variant (e.g., operational, denotational) or programming
paradigm (e.g., procedural, functional), hence we will use a general notion of
program semantics as a function that maps programs to arbitrary mathematical
objects. As argued in [Tur18, Chapter 10], this formalism, although usually
stated in the context of denotational semantics, can also incorporate
operational semantics (by mapping programs to functions on states).

We are also interested in comparing the high-level behaviour of programs, in
order to detect whether a program $P^{\prime}$ manifests (at least) the
behaviours of another program $P$. This can be achieved by a relation of
_simulation_ , or _inexact copy_ in the sense of [AP18], which uses a notion
of state-based simulation that results in a reflexive and transitive relation,
i.e., a preorder; here, we will only assume the algebraic properties of
simulation without being confined to a state-based definition.

A _semantical framework_ is a tuple
$(I,\mathord{\perp},\lVert\cdot\rVert,\preccurlyeq_{\text{sim}})$ where $I$ is
an arbitrary set of semantical objects, $\lVert\cdot\rVert\colon P\rightarrow
I$ maps each program to its _semantics_ , $\mathord{\perp}\in I$ is the value
to which non-valid programs are mapped, and the _simulation relation_
$\preccurlyeq_{\text{sim}}\subseteq I\times I$ is a preorder on $I$ with
$\mathord{\perp}$ as its minimum element. The empty program shall be treated
specially and be mapped to $\mathord{\perp}$, i.e.,
$\lVert\mathtt{e}\rVert=\mathord{\perp}$. Let $\mathcal{P}$ be the set of all
semantical frameworks. Let $(I,\lVert\cdot\rVert,\preccurlyeq_{\text{sim}})$
be a semantical framework. We extend the notation $\preccurlyeq_{\text{sim}}$
to programs by defining, for $p_{1},p_{2}\in P$, that
$p_{1}\preccurlyeq_{\text{sim}}p_{2}$ iff $\lVert
p_{1}\rVert\preccurlyeq_{\text{sim}}\lVert p_{2}\rVert$. Also, we write
$x\approx_{\text{sim}}y$ iff $x\preccurlyeq_{\text{sim}}y$ and
$y\preccurlyeq_{\text{sim}}x$ (alluding to the notion of bisimulation).

###  3.2. Reasoning about programs and the world

In our setting, verification of programs will be modelled via an (abstract)
notion of reasoning on program properties. This is more closely related to
formal verification, but, due to the abstractness of our definitions, it can
also be made to include descriptions of experimental verification results.

Let $H\subset S$ be a designated subset of $S$ that contains hypotheses. We
can think of these hypotheses as descriptions of program properties and
functionalities; as such, they can be used for modelling notions such as
functional specifications or formal reasoning on programs and properties of
the program’s environment. In an extended framework which would include
physical machines, hypotheses might be extended to also include relevant
statements about the physical world.

A _truth assignment_ is any function $u\colon
H\rightarrow\\{\,\mathrm{t},\mathrm{f},\mathord{?}\,\\}$ ($\mathrm{t}$ for
true, $\mathrm{f}$ for false, and $\mathord{?}$ for meaningless) such that
$u(\mathtt{e})=\mathord{?}$. Let $\mathcal{U}$ be the set of all truth
assignments.

Although we are using only three truth values, it could be conceivable to
extend the framework to use more truth values (perhaps organised in a
bilattice [Fit06]), in an attempt to model situations where programs might be
accepted as “fit for use”.

###  3.3. Specifications

Let $A$ be an arbitrary set of possible actions and $E$ be an arbitrary set of
possible evidence. Actions encode voluntary acts of software developing that
are under the control of the programmers. Evidence encode what can be observed
by the programmers. These sets will be different in any application of our
framework: for example, actions might contain the data of verification
attempts, encodings of some actual actions of the programmer, etc; evidence
might contain verification results (as an alternative of encoding them into
the hypotheses), encodings of (past or current) events, etc.

A central notion in our definition of specification will be that of a possible
world. In the words of [KJG92, Section III], a possible world “is the
component of truth that cannot be manipulated at will”. Hence, while the
programmer can (in principle) code, assume, and do whatever she pleases, the
world poses some semantical (and practical) limitations. This reflects the
discussion in Section 2.3 regarding the normative force of specifications over
programs, especially when taking into account that in the framework of [Ara17]
possible worlds have a similar force against scientific theories.

The term “possible world” is kept unchanged with respect to [Ara17] for one
more reason: as argued in [ZJ97, Section 3.2], specifications can be thought
of as containing only statements about the environment of the machine, either
per se or in relation to the machine; such a viewpoint is meant to aid in
avoiding implementation bias during the formulation of specifications. The
term “possible world” can serve as a subtle pointer to that viewpoint.

A _possible world_ is a function $w\colon P\times H\times
A\times\omega\rightarrow\mathcal{P}\times\mathcal{U}\times E$.

Hence, at each stage of software development, the world responds to the
current program, hypothesis, and action of the programmer by imposing the
semantics of the program, specifying what can be considered true, false, or
meaningles (for this specific programmer), and outputting a piece of evidence.
Notice that this is intended as a behavioural, not ontological, description of
our possible worlds; in other words, it is an _interface_ they must adhere to,
but the inner structure of a possible world might be different than a
function.

The fact that truth assignments and program semantics are decided by the
possible world at each time instance _depending on the actions of the program
generators_ gives the ability to incorporate what we dubbed _horizontal
relationism_ , because each program generator might perform actions that end
up in different truth or semantics; however, since they are controlled by the
world and not completely by the program generator, truth, meaning, and
evidence also have an objective side, reflecting the fact that these elements
depend also on factors not under the control of the software developers.

This definition does not use the most generic signature of possible worlds of
[KJG92, Section III.A]; such a signature would have as part of its input an
infinite sequence of $P\times H\times A$ tuples instead of a single $P\times
H\times A$ tuple, so as to allow the output to depend on the past actions of
the programmer (the part of the sequence with indexes before the time
argument) and the future actions of the programmer (the part of the sequence
with indexes after the time argument). However, for our purposes, the present
status seems to be enough, since possible worlds will be used as building
blocks of specifications. We consider specifications to be independent of
previous (and definitely of future) actions of programmers. Moreover, when
programs are compared to their specifications, they are compared to the
_current_ state of the specification. Note that, if we wished to model
specification change (and to do so accurately), we might have needed to resort
to dependence on the past, hence replace the $P\times H\times A$ tuple with a
finite sequence (having length equal to the time argument) of $P\times H\times
A$ tuples.

In the original framework of [Ara17], a set of possible worlds defines the
_background knowledge_ shared by two different generators of scientific
theories; the intuition behind this definition is that a property about the
actual world is equivalent to the set of possible worlds that exhibit it. We
will reinterpret the same construct, sets of possible worlds, as
specifications; similarly, the intuition will be that a property about the
program to be created is equivalent to the set of the worlds that specify it.

A _specification_ $K$ is a set of possible worlds.

Each possible world in a specification relaxes the behaviour of the program in
some (possibly different) ways; for example, world $w_{1}$ might allow the
program to be written in more programming languages, $w_{2}$ might omit a
temporal liveness property such as “for each user, a logout happens at most 5
minutes after a login”, $w_{3}$ might omit a temporal safety property such as
“no user that does not have the role Admin can access the control panel”, etc
(for a definition of safety and liveness properties, see, for example,
[AP22]). Hence, the intersection of all the properties that are present in all
the worlds corresponds to our usual intuition about specifications; this
statement will have its mathematical counterpart in the definition of theories
below.

The fact that the output of each possible world depends on time allows for a
(basic) form of specification change. Notice that this change does not depend
on the actions of any specific programmer; it is defined independently of the
interaction between world and programmer. Hence, specifications change
uniformly for all programmers following them.

###  3.4. Developing programs

We now turn to describing programmers. We will use the term _program
generator_ , in order to also be able to accommodate other kinds of entities,
such as teams of programmers or even automatic code generators. As with
possible worlds, our definition is to be read behaviourally, not
ontologically.

A _program generator_ is a function $\delta\colon
E^{\omega^{\star}}\rightarrow P\times H\times A$.

The structures of possible worlds and program generators allows them to
interact. At each point $n$ in time, a program generator $\delta$ is free to
review the historical evidence and, having done so, produces a program,
accompanied by a hypothesis regarding its functionality and its properties,
and performs some action. The world $w$ can then respond and, in the process,
create some fresh evidence. This allows the program generator to produce new
output at the next point in time. This process can be summarised in
mathematical notation as a sequence
$(p^{w,\delta}_{n},h^{w,\delta}_{n},u^{w,\delta}_{n},I^{w,\delta}_{n},\mathord{\perp}^{w,\delta}_{n},\lVert\cdot\rVert^{w,\delta}_{n},\preccurlyeq_{\text{sim}}^{w,\delta,n},a^{w,\delta}_{n},e^{w,\delta}_{n})_{n\in\omega}$,
where

$\displaystyle\left(p^{w,\delta}_{0},h^{w,\delta}_{0},a^{w,\delta}_{0}\right)=\delta\left(\emptyset\right),$
$\displaystyle\left((I^{w,\delta}_{n},\mathord{\perp}^{w,\delta}_{n},\lVert\cdot\rVert^{w,\delta}_{n},\preccurlyeq_{\text{sim}}^{w,\delta,n}),u^{w,\delta}_{n},e^{w,\delta}_{n}\right)=w\left(p^{w,\delta}_{n},h^{w,\delta}_{n},a^{w,\delta}_{n},n\right),$
$\displaystyle\left(p^{w,\delta}_{n+1},h^{w,\delta}_{n+1},a^{w,\delta}_{n+1}\right)=\delta\left(\left(e^{w,\delta}_{m}\right)_{m\leq
n}\right).$

Consider a setting where a programmer $\delta$ is using git [CS14] to store
code and wants to write a web application that has a control panel. According
to the specification, the web application must have a /login endpoint where
users can login; each user has a role and users that do not have role Admin
cannot access the control panel. Hence, each world of the specification
contains these properties, however different worlds might also allow more
behaviours.

$\delta$ has decided to work with the PHP programming language and validate
their program using linear temporal logic (which happens to be supported by
the specification) and automated tests. For each step, the current program is
a string of (hopefully well-formatted) PHP code; the hypothesis contains a
conjunction of the following properties (possibly among many other
properties), formally expressed in the selected logic:

  * •

For each request to endpoint /login, the response status is not an HTTP 404
Not found.

  * •

For each request to endpoints that start with /admin/, if the requesting user
does not have role Admin, then the response status is an HTTP 403 Forbidden or
an HTTP 401 Unauthorized.

Moreover, for each step, the action of $\delta$ contains a git commit and the
automated tests that are to be run.

The response of possible worlds to $\delta$ always includes the semantics of
PHP. Evidence contains the results of the tests and the changes to the git
repository (also, maybe a textual representation of the specification).
Regarding truth assignments, they map valid formulas of temporal logic to
truth values $\mathrm{t}$ and $\mathrm{f}$ and everything else to
$\mathord{?}$; the formulas that are mapped to $\mathrm{t}$ are exactly those
that are validated by the program and are consistent with what the possible
world allows.

[Software evolution à la [PRC21]] In [PRC21], a formal system based on belief
change is defined to reason about software evolution. In that system, a
specification is a propositional theory $\mathcal{S}_{m}$. The programmer
creates an intended implementation $\mathcal{I}$ of the specification. A
description $S_{i}$ of the implementation is then extracted from
$\mathcal{I}$, consisting of a set of propositional formulas (not necessarily
closed under logical consequence). The theory $\mathcal{S}_{m}$ and the
description $S_{i}$ can be compared in order to reason whether the
implementation satisfies the specification correctly (and whether the
entrenchment of properties relative to each other is as desired). In case
changes are required, $S_{i}$ is modified via some specific revision operators
(defined in [PRC21, Section 3]) and this results in a new $S_{i}^{\prime}$
which can be abstracted into a new $\mathcal{S}_{m}^{\prime}$. The new
specification can be then used by the programmer to create a new intended
implementation. A simplified form (ignoring entrenchment of properties) of
this formal system can be expressed in our framework as follows.

Since $\mathcal{S}_{m}$ expresses specific behaviours that the intended
software system _should_ display, its role is similar to that of a
specification in our setting. We can define each possible world $w$ to contain
a copy of $\mathcal{S}_{m}$.

$S_{i}$ represents a model of a specific implementation. In our setting, we
can use the conjunction of the formulas in $S_{i}$ as (part of) the hypothesis
at each time instant. Notice that, in such cases, where the hypothesis is
meant to contain a description of the program, it is the responsibility of the
possible world to check both that $S_{i}$ is indeed an accurate description of
the given program and that it conforms to the specification.

At each step of the process, any (or maybe the first encountered) possible
inconsistency between $\mathcal{S}_{m}$ and $S_{i}$ is encoded into the
evidence returned by the world, so that the programmer can react to it. In
this context, the revision operators can be considered as “recipes” that
program generators can follow to respond to evidence.

Contrary to [PRC21], which assumes that $\mathcal{S}_{m}$ might change at
every step of the process, our framework can only allow the update operations
to affect $S_{i}$. While specifications in our framework can change over time,
this change is uniform for all different program generators and hence should
not depend on the specifics of the workings of any single program generator;
more generally, specifications as normative entities (i.e., functional
specifications, such as $\mathcal{S}_{m}$) change quite more rarely and by
different kinds of procedures than specifications as descriptive entities
(i.e., system specifications, such as $S_{i}$).

The elements obtained during the interaction of program generators and
possible worlds can be used for defining other structures, which will be
useful when stating properties.

At each time instant $n$ and possible world $w$, the programmer $\delta$ is
presented with a truth assignment on possible hypotheses. Hence, there arises
a logical language (of program properties)

$L^{w,\delta}_{n}=\\{\,s\in
H\operatorname{\mid}u^{w,\delta}_{n}(s)\neq\mathord{?}\,\\}.$

Moreover, it is possible to define semantic entailment, both locally (in the
given possible world) and globally (over the whole specification).

Let $\delta$ be a program generator, $K$ a specification and $n\in\omega$.

  1. (1)

If $w$ is a possible world, for $r,s\in H$, we define
$\\{\,w\,\\},r\models^{\delta}_{n}s$ to be true iff
$u^{w,\delta}_{n}(r)=\mathrm{t}$ implies $u^{w,\delta}_{n}(s)=\mathrm{t}$.

  2. (2)

For $r,s\in H$, we define $K,r\models^{\delta}_{n}s$ to be true iff
$\\{\,w\,\\},r\models^{\delta}_{n}s$ for all $w\in K$.

Hence, every program generator $\delta$ in every possible world $w$ at every
$n\in\omega$ can be considered to possess a logic having $L^{w,\delta}_{n}$ as
sentences and $K$ as its (intended) models. This motivates the notion of a
(logical) _theory_ (of program properties): it is formed as the closure (over
global semantic entailment) of the current hypothesis, i.e.,

$T^{w,\delta,K}_{n}=\\{\,s\in
H\operatorname{\mid}K,h^{w,\delta}_{n}\models^{\delta}_{n}s\,\\}.$

Notice that, in general, $T^{w,\delta,K}_{n}$ may contain strings marked as
false by the current truth assignment; it may even not be a subset of
$L^{w,\delta}_{n}$.

Similarly to the logical definitions, we can define notions that relate to
programs; these will be the sets of semantically valid programs. The programs
that “make sense” locally (i.e., in the given possible world) for the program
generator are

$P^{w,\delta}_{n}=\\{\,\mathtt{e},p^{w,\delta}_{n}\,\\}\cup\\{\,p\in
P\operatorname{\mid}\mathord{\perp}^{w,\delta}_{n}\neq\lVert
p\rVert^{w,\delta}_{n}\,\\};$

they include the current program, in virtue of it being stated by the program
generator, even when it does not actually make sense semantically. On the
other hand, the programs that make sense globally (i.e., for the whole
specification) for the program generator are

$V^{K,\delta}_{n}=\\{\,p\in P\operatorname{\mid}\forall w\in
K,\mathord{\perp}^{w,\delta}_{n}\neq\lVert p\rVert^{w,\delta}_{n}\,\\}.$

Notice that memberhood in these sets is not determined by whether a program
meets the specification, but only by whether it is correctly formed in its
programming language. The question of whether the program meets its
specification is decided by the response of the world to the hypothesis that
accompanies the program.

######  Remark 2.

$V^{K,\delta}_{n}\subseteq P^{w,\delta}_{n}$ and $\mathtt{e}\notin
V^{K,\delta}_{n}$.

###  3.5. Properties of program generators

Although any kind of program generator is possible, even for example one that
always outputs nonsense, we will usually want to focus our discussion on
program generators that actually follow their specification correctly. As in
[Ara17], some properties can be defined that describe good behaviour of a
program generator at a specific time instant (and world). Sound methodologies
of programming should then correspond to rules that program generators can
follow in order to achieve, possibly not from scratch but hopefully from some
time onwards, the desired properties.

The simplest such desired property is that the current program must actually
be a valid program. Moreover, it is natural to ask that its behaviour is
correctly described by the current hypothesis, which, in addition, is
compatible with the specification. A more advanced property is that the
current theory fully describes (correctly) the behaviour of the current
program. These three properties are expressed in the next definition, followed
by some of their implications.

Let $\delta$ be a program generator, $K$ a specification, $w\in K$, and
$n\in\omega$.

The program generator $\delta$:

  1. (1)

_is valid at $n$, $w$ given specification $K$_ (notation
$\operatorname*{Valid}^{\delta,w,K}_{n}$) iff $p^{w,\delta}_{n}\in
V^{K,\delta}_{n}$,

  2. (2)

_is correct at $n$, $w$_ (notation $\operatorname*{Correct}^{\delta,w}_{n}$)
iff $u^{w,\delta}_{n}(h^{w,\delta}_{n})=\mathrm{t}$,

  3. (3)

_is complete at $n$, $w$ given specification $K$_ (notation
$\operatorname*{Complete}^{\delta,w,K}_{n}$) iff

$\\{\,s\in H\operatorname{\mid}u^{w,\delta}_{n}(s)=\mathrm{t}\,\\}\subseteq
T^{w,\delta,K}_{n},$

  4. (4)

_is mature at $n$, $w$ given specification $K$_ (notation
$\operatorname*{Mature}^{\delta,w,K}_{n}$) iff
$\operatorname*{Correct}^{\delta,w}_{n}$,
$\operatorname*{Valid}^{\delta,w,K}_{n}$, and
$\operatorname*{Complete}^{\delta,w,K}_{n}$.

######  Proposition 3.

If $\operatorname*{Correct}^{\delta,w}_{n}$, then
$T^{w,\delta,K}_{n}\subseteq\\{\,s\in
H\operatorname{\mid}u^{w,\delta}_{n}(s)=\mathrm{t}\,\\}$ (hence also
$T^{w,\delta,K}_{n}\subseteq L^{w,\delta}_{n}$).

######  Proof 3.1.

Let $s\in T^{w,\delta,K}_{n}$. Then, $K,p^{w,\delta}_{n}\models^{\delta}_{n}s$
and, a fortiori, $\\{\,w\,\\},h^{w,\delta}_{n}\models^{\delta}_{n}s$. Since
$u^{w,\delta}_{n}(h^{w,\delta}_{n})=\mathrm{t}$, it follows that
$u^{w,\delta}_{n}(s)=\mathrm{t}$.

######  Proposition 4.

If $\operatorname*{Mature}^{\delta,w,K}_{n}$, then
$T^{w,\delta,K}_{n}=\\{\,s\in
H\operatorname{\mid}u^{w,\delta}_{n}(s)=\mathrm{t}\,\\}$.

######  Proof 3.2.

Since $\operatorname*{Correct}^{\delta,w}_{n}$, Proposition 3 implies that
$T^{w,\delta,K}_{n}\subseteq\\{\,s\in
H\operatorname{\mid}u^{w,\delta}_{n}(s)=\mathrm{t}\,\\}$. The fact that
$\operatorname*{Complete}^{\delta,w,K}_{n}$ completes the argument.

###  3.6. Translations between the outputs of program generators

Since there might be multiple different program generators working on the same
specification, it is important to be able to compare their outputs. Among the
items created by the interaction of program generators and worlds, we are
mainly interested in comparing the programs and the theories on the programs.
On the other hand, actions and evidence are meant to be esoteric to the
interaction between world and program generator, hence those need not concern
us during comparisons. These considerations motivate the following definition.

Let $\gamma$ and $\delta$ be two program generators with common specification
$K$. For every possible worlds $w_{1},w_{2}\in K$ and stages $m$, $n$ of
development, we will say that the output of $\gamma$ is _translatable_ to the
output of $\delta$ (notation
$\left\langle\gamma\right\rangle_{m}^{w_{1}}\Rightarrow_{\mathrm{repr}}\left\langle\delta\right\rangle_{n}^{w_{2}}$)
iff there exists a _translation function_ $f^{w_{1}\rightarrow
w_{2},\gamma\rightarrow\delta}_{m\rightarrow n}\colon P^{w_{1},\gamma}_{m}\cup
L^{w_{1},\gamma}_{m}\rightarrow P\cup H$ such that

  1. (1)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(\mathtt{e})=\mathtt{e}$,

  2. (2)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(L^{w_{1},\gamma}_{m})\subseteq L^{w_{2},\delta}_{n}$

  3. (3)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(P^{w_{1},\gamma}_{m})\subseteq P^{w_{2},\delta}_{n}$,

  4. (4)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(p^{w_{1},\gamma}_{m})\preccurlyeq_{\text{sim}}^{w_{2},\delta,n}p^{w_{2},\delta}_{n}$,

  5. (5)

for $r,s\in L^{w_{1},\gamma}_{m}$, if
$\\{\,w_{1}\,\\},r\models^{\gamma}_{m}s$, then
$\\{\,w_{2}\,\\},f^{w_{1}\rightarrow
w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(r)\models^{\delta}_{n}f^{w_{1}\rightarrow
w_{2},\gamma\rightarrow\delta}_{m\rightarrow n}(s)$,

  6. (6)

for $p_{1},p_{2}\in P^{w_{1},\delta}_{m}$, if
$p_{1}\preccurlyeq_{\text{sim}}^{w_{1},\gamma,m}p_{2}$ then
$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(p_{1})\preccurlyeq_{\text{sim}}^{w_{2},\delta,n}f^{w_{1}\rightarrow
w_{2},\gamma\rightarrow\delta}_{m\rightarrow n}(p_{2})$,

  7. (7)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(T^{w_{1},\gamma,K}_{m})\subseteq T^{w_{2},\delta,K}_{n}$,

  8. (8)

$f^{w_{1}\rightarrow w_{2},\gamma\rightarrow\delta}_{m\rightarrow
n}(V^{K,\gamma}_{m})\subseteq V^{K,\delta}_{n}$.

Points 2 and 3 specify that the translation maps sentences to sentences and
programs to programs, while points 7 and 8 require that the same happens for
sentences in theories and for valid programs. Since there is a designated
string, the empty one, point 1 takes care of it.

Point 6 requires that a translation preserve program semantics. Of course,
source code meaningful in one setting may not be meaningful in another (for
example, $\gamma$ may operate in one programming language and $\delta$ in
another). Most importantly, however, programs may be mapped to different kinds
of mathematical objects in the two settings (for example, $\gamma$ may operate
in a functional paradigm and $\delta$ in a procedural paradigm), hence we can
only express preservation of program semantics indirectly, by the (weaker)
condition that translation must preserve the simulation relation.

Point 5 requires that a translation preserve logical entailment. Since,
contrary to the situation with programs, truth assignments have the same range
in all settings, we could have opted for the stronger condition
$u^{w_{1},\gamma}_{m}(s)=u^{w_{2},\delta}_{n}(f^{w_{1}\rightarrow
w_{2},\gamma\rightarrow\delta}_{m\rightarrow n}(s))$; however this would have
two important ramifications: firstly, it would complicate adding more truth
values (maybe for only some of the program generators), and, secondly, it
would prevent more mature agents from correctly reinterpreting the false
theories of their less mature counterparts.

Finally, point 3 requires that, for a successful translation, the program of
$\delta$ must be able to perform (at least) the operations of the translation
of the program of $\gamma$ (again, since the simulation relation might be
different in the two worlds, we can only compare indirectly).

######  Remark 5.

Translation functions compose: if $f^{w_{1}\rightarrow
w_{2},\beta\rightarrow\gamma}_{l\rightarrow m}$ and $f^{w_{2}\rightarrow
w_{3},\gamma\rightarrow\delta}_{m\rightarrow n}$ are translation functions,
then $f^{w_{1}\rightarrow w_{2},\beta\rightarrow\gamma}_{l\rightarrow
m}\mathbin{;}f^{w_{2}\rightarrow w_{3},\gamma\rightarrow\delta}_{m\rightarrow
n}$ is a translation function. Since the identity function is a translation
function, it follows that, given a specification $K$, a category of
translation functions arises.

######  Corollary 6.

If $f^{w\rightarrow w^{\prime},\gamma\rightarrow\delta}_{m\rightarrow n}$ is a
translation function and $f^{w^{\prime}\rightarrow
w,\delta\rightarrow\gamma}_{n\rightarrow m}$ is another translation function,
then

  1. (1)

$(f^{w\rightarrow w^{\prime},\gamma\rightarrow\delta}_{m\rightarrow
n}\mathbin{;}f^{w^{\prime}\rightarrow w,\delta\rightarrow\gamma}_{n\rightarrow
m})(p^{w,\gamma}_{m})\preccurlyeq_{\text{sim}}^{w,\gamma,m}p^{w,\gamma}_{m}$,

  2. (2)

$(f^{w\rightarrow w^{\prime},\gamma\rightarrow\delta}_{m\rightarrow
n}\mathbin{;}f^{w^{\prime}\rightarrow w,\delta\rightarrow\gamma}_{n\rightarrow
m})(T^{w,\gamma,K}_{m})\subseteq T^{w,\gamma,K}_{m}$.

######  Theorem 7.

Let $\gamma$ and $\delta$ be two program generators with common specification
$K$. For every possible world $w\in K$ and stages $m$, $n$ of development, if
$\operatorname*{Mature}^{\gamma,w_{1},K}_{m}$ and
$\operatorname*{Mature}^{\delta,w_{2},K}_{n}$, then
$\left\langle\gamma\right\rangle_{m}^{w_{1}}\Rightarrow_{\mathrm{repr}}\left\langle\delta\right\rangle_{n}^{w_{2}}$
or
$\left\langle\delta\right\rangle_{n}^{w_{2}}\Rightarrow_{\mathrm{repr}}\left\langle\gamma\right\rangle_{m}^{w_{1}}$.

######  Proof 3.3.

We will construct a (trivial) translation function $f$.

Of course, by maturity, both $L^{w_{1},\gamma}_{m}$ and $L^{w_{2},\delta}_{n}$
contain some true statement, namely, $h^{w_{1},\gamma}_{m}$ and
$h^{w_{2},\delta}_{n}$ respectively. Let $s_{\mathrm{t}}^{\gamma}$ be some
true statement in $L^{w_{1},\gamma}_{m}$ (any such statement is enough for
this proof, but if the set of all true statements is finitely generated by a
set $S$, we could set $s_{\mathrm{t}}^{\gamma}=\bigwedge S$; similar
considerations apply for $s_{\mathrm{t}}^{\delta}$) and
$s_{\mathrm{t}}^{\delta}$ some true statement in $L^{w_{2},\delta}_{n}$. If
there is no false statement in $L^{w_{1},\gamma}_{m}$ and no false statement
in $L^{w_{2},\delta}_{n}$, then we can define $\forall s\in
L^{w_{1},\gamma}_{m},f(s)=s_{\mathrm{t}}^{\delta}$. Otherwise, at least one of
the languages contains a false statement; without loss of generality, let that
language be $L^{w_{2},\delta}_{n}$ and let $s_{\mathrm{f}}^{\delta}\in
L^{w_{2},\delta}_{n}$ be the false statement. Then, we can define

$\forall s\in
L^{w_{1},\gamma}_{m},f(s)=\begin{cases}s_{\mathrm{t}}^{\delta}&\text{if
}u^{w_{1},\gamma}_{m}(s)=\mathrm{t}\\\
s_{\mathrm{f}}^{\delta}&\text{otherwise}\end{cases}$

In both cases, $u^{w_{1},\gamma}_{m}(s)=u^{w_{2},\delta}_{n}(f(s))$ for all
$s\in L^{w_{1},\gamma}_{m}$ and hence $f$ trivially validates point 3.6.5. By
definition, 3.6.2 is also valid for $f$. Finally, by correctness of $\gamma$,
$T^{w_{1},\gamma,K}_{m}\subseteq\\{\,s\in
S\operatorname{\mid}u^{w_{1},\gamma}_{m}(s)=\mathrm{t}\,\\}$ and hence
$f(T^{w_{1},\gamma,K}_{m})=\\{\,s_{\mathrm{t}}^{\delta}\,\\}$, so we obtain
3.6.7 by completeness of $\delta$.

As for programs, define

$\forall p\in
P^{w_{1},\gamma}_{m},f(p)=\begin{cases}p^{w_{2},\delta}_{n}&\text{if }\exists
p^{\prime}\in
V^{K,\gamma}_{m}:p^{\prime}\preccurlyeq_{\text{sim}}^{w_{1},\gamma,m}p\\\
\mathtt{e}&\text{otherwise}\end{cases}$

By definition, 3.6.1 and 3.6.3 hold for $f$. Since $\gamma$ is mature and the
simulation relations are reflexive, we obtain 3.6.4. By maturity of $\delta$
and the reflexivity of the simulation relation (of $\gamma$), 3.6.8 is also
true. For 3.6.6, let $p_{1},p_{2}\in P^{w_{1},\gamma}_{m}$ with
$p_{1}\preccurlyeq_{\text{sim}}^{w_{1},\gamma,m}p_{2}$; if
$f(p_{1})=\mathtt{e}$, then we are done; else,
$p^{\prime}\preccurlyeq_{\text{sim}}^{w_{1},\gamma,m}p_{1}$ for some
$p^{\prime}\in V^{K,\gamma}_{m}$, hence, by transitivity of the simulation
relation (of $\gamma$), $f(p_{1})=f(p_{2})$ and reflexivity of the simulation
relation (of $\delta$) completes the argument.

The triviality of the function constructed in the preceding theorem lies on
the fact that it has only four output values, thus eliminating, for example,
any differences in program behaviour and any relations between properties.
However, taking care of that would require possessing more information
regarding the inner structure of programs, theories, and the workings of
formulating theories of programs, hence it can only happen in more specific
instantiations of the framework.

By taking the conditions of the theorem in the limit, we obtain that two
program generators that asymptotically arrive at mature programs with respect
to a shared specification will asymptotically produce programs and theories
one of which can be translated into the other.

######  Corollary 8.

Let $\gamma$ and $\delta$ be two program generators with common specification
$K$. If for every $w\in K$,
$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\operatorname*{Mature}^{\gamma,w,K}_{n}$
and
$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\operatorname*{Mature}^{\delta,w,K}_{n}$,
then for every $w\in K$,

$\mathbf{\operatorname*{\mathbf{lim}}}_{n\rightarrow\infty}\left\langle\gamma\right\rangle_{n}^{w}\Rightarrow_{\mathrm{repr}}\left\langle\delta\right\rangle_{n}^{w}\vee\left\langle\delta\right\rangle_{n}^{w}\Rightarrow_{\mathrm{repr}}\left\langle\gamma\right\rangle_{n}^{w}.$

##  4\. Conclusion

Similar to [Ara17], the central elements of the framework on its technical
level (corresponding to the central elements of specifications and software
developers on the conceptual level) are _possible worlds_ and _program
generators_ and we are studying their interaction. At each time instance, a
program generator processes the evidence up to the given time and produces a
program, a hypothesis, and an action. The possible world responds with a truth
assignment, program semantics, and some new evidence; the new evidence can be
appended to the existing and be fed into the program generator at the next
time instance, continuing the interaction.

Using these elements above, we have defined an abstract notion of
translatability between the outputs of programmers working in different
settings. As a token of the importance of such a notion, we have shown,
similarly to [Ara17], that two program generators starting with common
specification (i.e., set of possible worlds) and writing correct programs
relative to that specification will end up in programs one of which can be
(trivially) translated into the other. Specific instantiations of the
framework can refine the definition of translatability we have provided and
thus, by adapting our proof accordingly, arrive at translations with more
specific structure.

The fact that we could adapt a framework targetted at describing natural
science and end up with a framework that describes software development and
still highly resembles its origin hints on the similarities between the two
endeavours. However, notice that, in addition to introducing new elements to
account for the technical artefacts that are produced by programmers, we had
to reinterpret some terms of the original framework in order to adapt it for
our purposes, most notably _background knowledge_ was reinterpreted as
_specification_ ; this is a hint of (one of) the key differences between the
two endeavours.

Of course, as already stated in Section 2, our framework does not handle all
the aspects of software development, let alone of the development of full
computational systems. We have commented on a few of the ways that it might be
extended to accommodate more such aspects. In addition, the reasoning on
logics of program generators might benefit if it is described via the theory
of institutions, an abstraction of model theory based on category theory;
[Dim] has already attempted such a modification of the original framework of
[Ara17]. Moreover, other kinds of mappings between the outputs of program
generators could be considered instead of translations, such as conceptual
blending [Gog99]; this might model the creative process of merging interesting
ideas from one program to the other while the programs are still expressed in
different formalisms.

## References

  * [AB89] Aristidis Arageorgis and Aristides Baltas.  Demarcating technology from science: Problems and problem solving in technology.  Journal for General Philosophy of Science, 20(2):212–229, September 1989.  doi:10.1007/BF01801475.
  * [Ang13] Nicola Angius.  Abstraction and Idealization in the Formal Verification of Software Systems.  Minds and Machines, 23(2):211–226, May 2013.  doi:10.1007/s11023-012-9289-8.
  * [Ang14] Nicola Angius.  The Problem of Justification of Empirical Hypotheses in Software Testing.  Philosophy & Technology, 27(3):423–439, September 2014.  doi:10.1007/s13347-014-0159-6.
  * [Ang20] Nicola Angius.  On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification.  Philosophy & Technology, 33(2):349–355, June 2020.  doi:10.1007/s13347-019-00364-9.
  * [AP18] Nicola Angius and Giuseppe Primiero.  The logic of identity and copy for computational artefacts.  Journal of Logic and Computation, 28(6):1293–1322, September 2018\.  doi:10.1093/logcom/exy012.
  * [AP22] Nicola Angius and Giuseppe Primiero.  Copying safety and liveness properties of computational artefacts.  Journal of Logic and Computation, August 2022.  doi:10.1093/logcom/exac053.
  * [APT21] Nicola Angius, Giuseppe Primiero, and Raymond Turner.  The Philosophy of Computer Science.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, spring 2021 edition, 2021.  URL: https://plato.stanford.edu/archives/spr2021/entries/computer-science/.
  * [Ara17] Aristidis Arageorgis.  Relativism, translation, and the metaphysics of realism.  Philosophical Studies, 174(3):659–680, March 2017.  doi:10.1007/s11098-016-0702-7.
  * [CS14] Scott Chacon and Ben Straub.  Pro git.  Apress, 2014.
  * [Dim] Maria M. Dimarogkona.  PhD thesis, School of Applied Mathematical and Physical Science, National Technical University of Athens.  To appear.
  * [DMP18] Liesbeth De Mol and Giuseppe Primiero.  What is a program? Historical and Philosophical perspectives.  The Reasoner, 12(2):11–12, February 2018.
  * [Fit06] Melvin Fitting.  Bilattices Are Nice Things.  In T. Bolander, V. Hendricks, and S. A. Pedersen, editors, Self-Reference. CSLI Publications, 2006.
  * [Flo16] Luciano Floridi.  The method of abstraction.  In Luciano Floridi, editor, The Routledge handbook of philosophy of information, Routledge handbooks in philosophy, pages 50–56. Routledge, Taylor & Francis Group, London New York, 2016.
  * [Gog99] Joseph Goguen.  An Introduction to Algebraic Semiotics, with Application to User Interface Design.  In Chrystopher L. Nehaniv, editor, Computation for Metaphors, Analogy, and Agents, Lecture Notes in Computer Science, pages 242–291, Berlin, Heidelberg, 1999. Springer.  doi:10.1007/3-540-48834-0_15.
  * [Gru11] Stefan Gruner.  Problems for a Philosophy of Software Engineering.  Minds and Machines, 21(2):275–299, May 2011.  doi:10.1007/s11023-011-9234-2.
  * [KJG92] Kevin T. Kelly, Cory Juhl, and Clark Glymour.  Reliability, Realism, and Relativism.  1992\.
  * [PRC21] Giuseppe Primiero, Franco Raimondi, and Taolue Chen.  A theory of change for prioritised resilient and evolvable software systems.  Synthese, 198(23):5719–5744, October 2021.  doi:10.1007/s11229-019-02305-7.
  * [Pri16] Giuseppe Primiero.  Information in the Philosophy of Computer Science.  In Luciano Floridi, editor, The Routledge handbook of philosophy of information, Routledge handbooks in philosophy, pages 90–106. Routledge, Taylor & Francis Group, London New York, June 2016.
  * [Tur11] Raymond Turner.  Specification.  Minds and Machines, 21(2):135–152, May 2011.  doi:10.1007/s11023-011-9239-x.
  * [Tur18] Raymond Turner.  Computational Artifacts: Towards a Philosophy of Computer Science.  Springer, Berlin, Heidelberg, 1st edition, 2018.  doi:10.1007/978-3-662-55565-1.
  * [Tur20] Raymond Turner.  Computational Intention.  Studies in Logic, Grammar and Rhetoric, 63(1):19–30, September 2020\.  doi:10.2478/slgr-2020-0025.
  * [ZJ97] Pamela Zave and Michael Jackson.  Four dark corners of requirements engineering.  ACM Transactions on Software Engineering and Methodology, 6(1):1–30, January 1997.  doi:10.1145/237432.237434.