计算机科学哲学 computer science, philosophy of (Nicola Angius, Giuseppe Primiero, and Raymond Turner)

首次发表于 2013 年 8 月 20 日星期二；实质性修订于 2021 年 1 月 19 日星期二

计算机科学哲学关注于计算机科学学科内部产生的本体论和方法论问题，以及软件开发及其商业和工业部署的实践。更具体地说，计算机科学哲学考虑了计算系统的本体论和认识论，重点关注与其规范、编程、实现、验证和测试相关的问题。计算机程序的复杂性确保了计算机科学哲学提出的许多概念问题与数学哲学、经验科学哲学和技术哲学中的问题相关。我们将在第 1 至 5 节提供反映计算系统本体论分层性质的主题分析；然后在第 6 至 8 节讨论涉及其方法论的主题。

---

计算系统

计算系统在日常生活中广泛存在。它们的设计、开发和分析是计算机科学学科的研究对象。计算机科学的哲学则将其视为理论分析的对象。其首要目标是定义这些系统，即发展计算系统的本体论。文献提供了关于这一主题的两种主要方法。第一种方法将计算系统理解为由软件和硬件的不同本体论定义，通常被视为它们的基本组成部分。另一种方法将计算系统视为围绕软件-硬件二分法的几个其他元素组成：根据这第二种观点，计算系统是基于一种抽象级别层次的层次结构定义的，将硬件级别排在这种层次结构的底部，并向上延伸到设计元素，向下延伸到包括用户在内。接下来我们将介绍这两种方法。

1.1 软件和硬件

通常，计算系统被视为由两个本体上不同的实体组成：软件和硬件。算法、源代码和程序属于第一类抽象实体；微处理器、硬盘驱动器和计算机则是具体的物理实体。

Moore (1978) 认为，这种二元性是计算机科学的三个神话之一，即软件/硬件的二分具有实用意义，但并非本体意义。计算机程序作为计算机可以执行的一组指令，可以在符号水平上（编码指令）和物理水平上（存储在物理介质中的指令）进行检查。 Moore 强调，没有程序存在为纯抽象实体，也就是说，没有物理实现（例如闪存驱动器、服务器上的硬盘，甚至一张纸）。早期的程序甚至直接硬连线，而在计算机时代初期，程序仅由物理杠杆的模式组成。通过软件/硬件对立，人们通常将软件与程序的符号水平，硬件与相应的物理水平相对应。然而，这种区别只能在实用上得到证明，因为它界定了开发人员的不同任务。对于他们来说，软件可以由算法和实现它们的源代码给出，而硬件则由机器代码和能够执行它的微处理器给出。相比之下，实现硬连线程序的工程师可能倾向于将计算机的许多物理部分称为软件。换句话说，对于一个专业人士来说算作软件的东西，对于另一个专业人士来说可能算作硬件。

Suber (1988) 更进一步地认为，硬件是一种软件。软件被定义为任何可被阅读和执行的模式：一旦人们意识到所有物理对象都展示出模式，就不得不接受硬件作为物理对象也是软件的结论。Suber 将模式定义为“任何明确的结构，不是狭义上需要一些重复、规律或对称性”（1988, 90），并认为任何这样的结构确实可以被阅读和执行：对于任何明确的模式，即使没有赋予任何含义，总是可以构想出一种语法和语义赋予意义，从而使模式成为可执行程序。

Colburn (1999, 2000) 在将软件和硬件区分开来的同时强调，前者具有双重性质，即它是一种“具体抽象”，既抽象又具体。要定义软件，需要参考“描述媒介”，即用于表达算法的语言，以及“执行媒介”，即构成硬件的电路。虽然软件始终是具体的，因为没有软件不依托于某种物理媒介的具体化，但它仍然是抽象的，因为程序员在开发活动中不考虑实现机器：他们更愿意开发可由任何机器执行的程序。这一方面被 Colburn (1999) 称为“内容的扩展”，并将计算机科学中的抽象定义为“内容的抽象”：内容被扩展而不是删除，就像数学抽象那样。

Irmak (2012) 批评了 Colburn (1999, 2000) 提出的软件的双重性质。他认为抽象实体缺乏时空属性，而具体意味着具有这些属性。因此，将软件定义为具体的抽象将意味着软件具有矛盾的属性。软件确实具有时间属性：作为人类创造的对象，一旦构想和实施，它就开始存在；它可以在某个后续时间停止存在。当所有副本被销毁，它们的作者死亡，没有其他人记得相应的算法时，软件就会停止存在。作为人类创造的对象，软件是一种工艺品。然而，软件在空间属性上缺乏，因为它无法与任何具体的实现相对应。销毁给定软件的所有物理副本并不意味着特定软件停止存在，正如上文所述，删除所有以某种高级语言实现软件算法的文本也不会。因此，软件是一种具有时间属性的抽象实体。基于这些理由，Irmak (2010) 将软件定义为一种抽象工艺品。

Duncan (2011)指出，区分软件和硬件需要比涉及简单的抽象/具体二分法更精细的本体论。 Duncan (2017)旨在通过关注 Turner（2011）关于规范的概念，即作为表达给出程序正确性条件的表达（见 §2），提供这样的本体论。 Duncan (2017)强调，程序也作为实现机器的规范，这意味着程序规定了机器需要执行的所有正确行为。如果机器与程序的行为不一致，就说机器发生故障，就像不符合规范的程序被称为有缺陷或包含错误一样。定义软件/硬件区别的另一个本体论类别是工件，Duncan (2017)将其定义为一种物理、时空实体，它被构建以实现某些功能，并且有一个社区认可该工件作为服务于该目的。也就是说，软件被定义为一组编码在某种编程语言中的指令，这些指令作为能够读取这些指令的工件的规范；硬件被定义为其功能是执行指定计算的工件。

1.2 抽象级别方法

如上所示，软件和硬件之间的区别并不是非常明显的。对计算系统的不同本体论方法依赖于抽象的作用。抽象是计算机科学中的一个关键元素，它有许多不同的形式。Goguen & Burstall（1985）描述了其中的一些变体，以下是一些例子。在编程过程中，代码可以通过命名文本和参数来重复，这种做法被称为过程抽象。这种操作在 lambda 演算的抽象操作中有其形式基础（请参阅 lambda 演算的条目），并且它允许一种称为多态性的形式机制（Hankin，2004）。另一个例子是类型化，这是函数式编程的典型特征，它为语言的语法构造器提供了一种表达系统。又或者，在面向对象设计中，模式（Gamma 等，1994）从软件系统中发现的常见结构中抽象出来，并用作对象的实现和规范之间的接口。

所有这些例子都共享一个基础方法论，即抽象层次（以下简称 LoA），在数学（Mitchelmore 和 White，2004 年）和哲学（Floridi，2008 年）中也被使用。数学中的抽象概念被堆叠在一起，不断寻求更加抽象的概念。根据这一观点，抽象是自包含的：抽象的数学对象仅从其定义的系统中获得意义，唯一的约束是新对象必须相互关联在一个一致的系统中，可以在没有参考先前或外部含义的情况下进行操作。一些人认为，在这方面，计算机科学中的抽象与数学中的抽象基本上是不同的：计算抽象必须留下一个实现痕迹，这意味着信息被隐藏但并未被销毁（Colburn 和 Shute，2007 年）。在一个 LoA 中忽略的任何细节都不应该被较低的 LoA 中的一个忽略：例如，程序员无需担心与特定变量关联的内存位置，但虚拟机需要处理所有内存分配。抽象依赖于不同层次的这种依赖反映在计算系统依赖于实现的属性上：例如，即使类隐藏了其方法的细节，它们也必须有实现。因此，计算抽象既保留了抽象的外观，又保留了实现。

LoAs 对数字计算系统本体论的完整表述已在 Primiero (2016)中设计出，包括：

• 意图

• 规范

• 算法

• 高级编程语言指令

• 汇编/机器码操作

• 执行

意图是定义要解决的计算问题的认知行为：它制定了创建计算过程以执行特定任务的请求。这种请求通常由参与特定软件开发项目的客户、用户和其他利益相关者提供。规范是制定解决手头计算问题所需的一组要求：它涉及可能的正式确定软件必须执行的操作，通过所知的需求获取过程。算法表达了提供解决方案给所提出的计算问题的过程，这个过程必须满足规范的要求。高级编程语言（如 C、Java 或 Python）指令构成了所提出算法的语言实现，通常称为源代码，它们可以被训练有素的程序员理解，但不能直接由计算机执行。用高级语言编码的指令通过编译器编译，即翻译成汇编代码，然后组装成机器码操作，可由处理器执行。最后，执行 LoA 是运行软件的物理级别，即执行指令的计算机体系结构。

根据这一观点，单独采用的任何抽象层次（LoA）都无法定义计算系统是什么，也无法确定如何区分软件和硬件。计算系统更多是由整个抽象层次结构来定义；每个抽象层次本身表达了与实现相关联的语义层次，无论是语言还是物理层面。

2. 意图和规范

意图指的是计算系统之外的认知状态，它表达了待解决的计算问题的制定。规范描述了待开发的计算系统必须满足的功能。虽然意图本身在计算机科学哲学内部并不引起特定的哲学争议，但在规范的定义以及规范与意图之间的关系方面会出现问题。

2.1 意图

意图阐明了确定计算系统是否合适的标准（即正确性，请参见 §7），因此被认为是计算系统适用于该问题的第一个 LoA。例如，客户和用户可能需要一款能够过滤掉来自呼叫中心的烦人电话的智能手机应用程序；这样的请求构成了在开发能够执行此任务的计算系统时的意图 LoA。在非幼稚系统的软件开发过程中，意图通常通过头脑风暴、调查、原型制作，甚至焦点小组（Clarke 和 Moreira，1999）等技术收集，旨在定义各利益相关者意图的结构化集合。在这个 LoA 中，没有提及如何解决计算问题，而只提供了必须解决的问题的描述。

在当代文献中，自 Anscombe (1963) 以来，意图一直是哲学探讨的对象。哲学家们研究了“行动的意图”（Davidson 1963），未来做某事的意图（Davidson 1978），以及有意识的行动（Anscombe 1963，Baier 1970，Ferrero 2017）。关于这三种意图中哪一种是主要的问题，它们如何相互联系，意图与信念之间的关系，意图是否是或预设特定的心理状态，以及意图是否作为行动的原因（参见有关意图的条目）。更正式的问题涉及一个代理人拥有不一致的意图的机会，但仍被认为是理性的（Bratman 1987，Duijf 等，2019）。

在计算系统本体论中作为第一层次的意图，意图可以被确认为未来的意图，因为它们表达了构建能够执行某些期望的计算任务的系统的目标。由于意图仅限于定义要解决的计算问题，而不指定其计算解决方案，它们的本体论和认识论分析与哲学文献中提到的并无不同。换句话说，在定义计算系统的意图中，并没有什么特别的计算内容值得在计算机科学哲学中单独处理。重要的是意图与规范之间的关系，因为意图为规范提供了正确性标准；规范被要求表达意图提出的计算问题应该如何解决。

2.2 定义和规范

再次考虑呼叫过滤应用程序的例子；一个规范可能要求创建一个与呼叫中心相关的电话号码黑名单；每隔 n 天更新列表；在有来电时检查号码是否在黑名单上；在肯定答复的情况下向呼叫管理系统通信，不允许来电进入；在否定答复的情况下允许来电。

后者是一个完整的规范，尽管用自然语言表达。规范通常用自然语言提出，以更接近利益相关者的意图，然后才在适当的形式语言中形式化。规范可以通过图形语言（如 UML（Fowler 2003））或更正式的语言（如 TPL（Turner 2009a）和 VDM（Jones 1990））来表达，使用谓词逻辑，或 Z（Woodcock 和 Davies 1996），侧重于集合论。例如，类型谓词逻辑（TPL）使用谓词逻辑公式表达计算系统的要求，其中指定了量化变量的类型。变量类型的选择允许在更合适的抽象级别上定义规范。规范是以非正式还是正式的形式表达往往取决于所遵循的开发方法，正式规范通常在正式开发方法的背景下更受青睐。此外，正式规范有助于验证计算系统的正确性（见第 6 节）。

Turner (2018)问道，在计算机科学中广泛使用的模型和规范之间有何区别。区别在于 Turner (2011)所称的“故意立场”：模型描述了一个打算开发的系统，如果两者之间存在不匹配，模型将被细化；规范则规定了系统应如何构建以符合预期功能，如果存在不匹配，系统将需要被细化。模型与系统之间的匹配反映了意图之间的对应关系——描述了系统应如何构建以解决计算问题——和规范——确定系统应如何构建，以满足解决计算问题所需的一组要求，如呼叫过滤应用程序的示例所示。用 Turner (2011)的话说，“当某物对工件的正确性具有管辖权时，它就是一个规范”：规范为计算系统提供正确性标准。因此，计算系统在遵守其规范时是正确的，也就是说，当它们按照规范行事时。相反，它们提供了故障的标准（§7.3）：计算系统在不与其规范一致时发生故障。Turner (2011)注意到，这样对规范的定义是一种理想化：在某些情况下，规范本身会被修订，比如当指定的计算系统由于物理定律的限制或成本限制而无法实现，或者当发现高级规范并非客户和用户意图的正确形式化时。

更一般地说，正确性问题不仅涉及规范，还涉及定义计算系统的任何两个 LoAs，正如下一小节将要讨论的那样。

2.3 规格和功能

完全实现和构建的计算系统是技术工件，即人造系统，旨在实现特定功能（Kroes 2012）。这样定义的技术工件包括桌子、螺丝刀、汽车、桥梁或电视机，它们与自然物体（如岩石、猫或二氢氧化物分子）以及艺术品有着明显区别，后者不具备功能。因此，计算系统的本体论属于技术工件的范畴（Meijers 2000），其特点是二元性，因为它们既由功能性属性定义，又由结构性属性定义（Kroes 2009，另请参阅有关技术哲学的条目）。功能性属性规定了工件需要执行的功能；结构性属性表达了工件可以执行这些功能的物理属性。以螺丝刀为例：功能性属性可能包括拧和松螺丝的功能；结构性属性可以指代一个能够插入螺丝头的金属片和一个允许顺时针和逆时针运动的塑料手柄。功能可以通过其结构对应物以多种方式实现。例如，螺丝刀的功能可以通过全金属螺丝刀或具有非常不同结构属性的电动螺丝刀来实现。

计算系统的分层本体论，其特征是许多不同的 LoAs，似乎延伸了定义技术工件的双重本体论（Floridi 等人，2015 年）。Turner（2018 年）认为，计算系统仍然是（Kroes 2009, 2012）意义上的工件，因为每个 LoA 对于较低的 LoAs 是功能级别，对于较高的 LoAs 是结构级别。

• 意图表达了系统必须实现的功能，并由规范实现；

• 规范发挥功能作用，详细解释软件必须实现的具体功能，并由算法实现，其结构水平

• 算法表达了高级语言程序必须实现的程序，即其结构级别

• 在高级语言中的指令定义了实现这些功能属性的机器语言代码

• 机器码最终表达了由执行级别实现的功能属性，这些属性表达了物理结构属性。

根据 Turner (2018) 的观点，结构层级不一定是物理层级，抽象工件的概念在计算机科学中也适用。因此，Turner (2011) 将高级语言程序本身定义为技术工件，因为它们构成一个实现规范的结构层级作为其功能层级（见 §4.2）。

第一个结果是，每个 LoA（表达要实现的功能）可以通过多种潜在的结构层次来实现，这些结构层次表达了如何实现这些功能：一个预期的功能可以通过多种方式来实现；通过规范表达的计算问题有多种不同算法的解决方案，这些算法在一些重要属性上可能有所不同，但都是同样有效的（见 §3）；一个算法可以在不同的程序中实现，每个程序用不同的高级编程语言编写，如果它们实现相同的算法，则都表达相同的程序（Angius 和 Primiero，2019）；源代码可以被编译成多种机器语言，采用不同的 ISA（指令集架构）；可执行代码可以安装并在多种计算机上运行（前提是这些计算机共享相同的 ISA）。

第二个结果是，每个 LoA 作为一个功能级别为更低级别提供了正确性标准（Primiero 2020）。不仅在实现级别上，从规范到执行的任何 LoA 都需要正确性，并且故障的原因可能在于任何 LoA 未正确实现其适当的功能级别（参见 §7.3 和 Fresco，Primiero（2013））。根据 Turner（2018）的说法，规范级别可以根据意图而言是正确的或不正确的，尽管验证其正确性可能会很困难。任何非物理层的正确性都可以通过形式验证在数学上进行验证，执行物理层可以通过测试进行经验验证（§6）。验证规范与客户意图的正确性将需要访问相关代理人的心理状态。

这个问题与建立工具如何具有功能以及结构属性如何与代理人的意图相关的更一般问题有关。这个问题在生物哲学和认知科学中也是众所周知的，有两种主要理论被提出作为解决方案。根据功能因果理论（Cummins 1975），功能由工具的物理能力决定：例如，心脏收缩和扩张的物理能力决定了它在循环系统中泵血的功能。然而，当应用于技术工具时，这个理论面临严重问题。首先，它阻止了定义正确性和故障（Kroes 2010）：假设我们手机上安装的来电过滤应用开始禁止来自手机通讯录联系人的电话，根据功能因果理论，这将是应用的一个新功能。其次，这个理论没有区分预期功能和副作用（Turner 2011）：在通话时间较长的情况下，我们的手机肯定会开始发热；然而，这并不是客户或开发人员预期的功能。根据功能意图理论（McLaughlin 2001，Searle 1995），由设计者或用户确定的功能是工具的预期功能，工具的结构属性被选择为能够实现这一功能。这个理论能够解释正确性和故障，以及区分副作用和预期功能。然而，它没有说明功能实际存在于哪里，是在工具中还是在代理人的头脑中。在前一种情况下，人们又回到了工具如何具有功能的问题。在后一种情况下，需要进一步解释心理状态如何与工具的物理属性相关（Kroes 2010）。Turner（2018）认为，功能因果理论和功能意图理论背后的直觉对于理解计算系统中功能和结构之间的关系是有用的，并建议将这两种理论合并为一个。一方面，没有实现就没有功能；另一方面，没有客户、开发人员和用户就没有意图。

3. 算法

尽管自古以来已为人所知并广泛使用，但关于算法的定义问题仍然是开放的（Vardi 2012）。“算法”一词源自于九世纪波斯数学家阿布·贾法尔·穆罕默德·本·穆萨·哈瓦里兹米的名字，他提供了使用阿拉伯数字进行算术运算的规则。事实上，人们遵循的计算基本算术运算（如乘法或除法）的规则是算法的日常示例。其他众所周知的例子包括使用圆规和直尺平分角度的规则，或者欧几里得算法用于计算最大公约数。直觉上，算法是一组指令，允许完成给定任务。尽管在数学中存在这种古老传统，但只有现代逻辑和哲学思考提出了提供算法定义的任务，这与二十世纪初数学基础危机有关（请参阅有关数学哲学的条目）。有效可计算性的概念起源于逻辑研究，为直观算法概念提供了一些形式上的对应，并催生了计算理论。从那时起，人们提出了不同的算法定义，从形式化到非形式化方法，如下一节所述。

3.1 古典方法

马尔可夫（1954 年）提供了算法的第一个精确定义，即作为一种确定的、适用的和有效的计算过程。如果涉及的指令足够精确，不允许在执行过程中出现任何“任意选择”，则计算过程是确定的。 （人类或人工）计算机绝不能对下一步该执行什么步骤感到不确定。对于马尔可夫来说，算法适用于输入类别（基本算术运算的自然数），而不是单个输入（特定自然数）。马尔可夫（1954 年：1）将效率定义为“算法获得特定结果的倾向”。换句话说，算法是有效的，因为它最终将产生计算问题的答案。

Kleene (1967) 将有限性规定为另一个重要属性：算法是一种可以用有限一组指令描述的过程，并且需要有限步骤来解决计算问题。举个反例，考虑一个由有限步骤定义的 while 循环，但由于循环中的条件始终满足，它会永远运行。指令还应该适合机械执行，也就是说，机器在执行指令时不需要洞察力。在遵循马尔可夫的确定性和加强有效性之后，Kleene (1967) 还规定指令应该能够识别计算问题的解已经得到，并停止计算。

Knuth (1973)回顾并深化了 Markov (1954)和 Kleene (1967)的分析，指出：

除了仅仅是一组规则的有限集合，用于解决特定类型问题的操作序列外，算法具有五个重要特征：

1. 有限性。算法必须在有限步之后终止。 [...]

2. 确定性。算法的每一步必须被准确定义；必须为每种情况严格和明确地指定要执行的操作。[…]

3. 输入。一个算法有零个或多个输入。[…]

4. 输出。一个算法可以有零个或多个输出。[…]

5. 有效性。算法通常也被期望是有效的，即其操作必须都足够基本，以至于原则上可以由使用纸和铅笔的人在有限的时间内准确完成。(Knuth 1973: 4–6)

正如 Kleene（1967）所述，有限性影响了指令数量和实现的计算步骤数量。与马尔可夫的确定性一样，Knuth 的确定性原则要求每个连续的计算步骤都必须明确定义。此外，Knuth（1973）更明确地要求算法具有（可能为空的）输入和输出集。Knuth 可能指的是没有输入或输出的算法，这些算法使用内部存储的数据作为输入，或者不将数据返回给外部用户（Rapaport 2019，第 7 章，在其他互联网资源中）。至于有效性，除了马尔可夫倾向于“获得特定结果”之外，Knuth 要求结果在有限时间内获得，并且指令是原子的，即足够简单，可以被人类或人工计算机理解和执行。

3.2 正式方法

Gurevich (2011)认为，一方面，提供算法的形式定义是不可能的，因为这个概念随着时间的推移不断发展：考虑古代数学中使用的顺序算法如何被当前计算机科学实践中的并行、模拟或量子算法所取代，以及新型算法可能在不久的将来被构想出来。另一方面，如果只关注经典的顺序算法，可以进行形式化分析。特别是，Gurevich (2000)为这类算法提供了公理化定义。

任何顺序算法都可以通过满足三个公理的顺序抽象状态机来模拟：

1. 顺序时间假设将任何算法 A 关联到一组状态 S(A)，一组初始状态 I(A) 是 S(A) 的子集，并且从 S(A) 到 S(A) 的映射是 A 的一步转换。状态是运行算法的快照描述。A 的运行是从某个初始状态开始的（可能是无限的）状态序列，使得从一个状态到其在序列中的后继状态有一步转换。Gurevich 的定义并不预设终止。一步转换不一定是原子的，但它们可能由有限的原子操作组成。

2. 根据抽象状态假设，S(A)中的状态是一阶结构，如数理逻辑中通常定义的那样；换句话说，状态为一阶语句提供语义。

3. 最后，有界探索假设陈述了对于 A 的两个状态 X 和 Y，总是存在一组术语 T，使得当 X 和 Y 在 T 上重合时，X 的更新集合对应于 Y 的更新集合。当 X 和 Y 在 T 上重合时，对于 T 中的每个术语 t，X 中 t 的评估与 Y 中 t 的评估相同。这使得算法 A 只探索与 T 中术语相关的状态部分。

Moschovakis (2001) 反对认为抽象机器并未完全捕捉到算法的直观概念。对于定义在自然数上的一般递归函数 f: ℕ → ℕ，通常有许多不同的算法可以计算它；“基本的、与实现无关的属性”并未被抽象机器所捕捉，而是通过一组递归方程来描述。以归并排序算法为例；有许多不同的归并排序抽象机器，问题是应该选择哪一个作为归并排序算法。归并排序算法实际上是指规定所涉及函数的一组递归方程，而归并排序过程的抽象机器则是相同算法的不同实现。Moschovakis 的形式分析提出了两个问题：相同算法的不同实现应该是等效的实现，然而，算法实现之间的等价关系需要进行正式定义。此外，仍需澄清通过递归方程系统形式化的算法直观概念究竟是什么。

Primiero (2020) 提出了对算法性质的三个不同抽象级别的阅读。在非常高的抽象级别上，算法可以被定义为从它们描述的过程中抽象出来，允许许多不同的状态集合和转换。在这个抽象级别上，算法可以被理解为非正式规范，也就是说，作为过程 P 的非正式描述。在较低的抽象级别上，算法指定了解决给定计算问题所需的指令；换句话说，它们指定了一个过程。因此，算法可以被定义为过程，或者是在某种给定形式语言 L 中描述如何执行过程 P 的描述。算法的许多重要属性，包括与复杂度类和数据结构相关的属性，在过程级别上无法确定，而是需要参考实现过程的抽象机器。在最底层的抽象级别上，算法可以被定义为可实现的抽象机器，即在形式语言 L 中，为给定抽象机器 M 的程序 P 的执行的规范。算法的三重定义使 Primiero (2020) 能够提供关于算法的等价关系的形式定义，这些定义涉及模拟和双模拟的代数概念（Milner 1973，另请参见 Angius 和 Primero 2018）。如果执行程序 Pi 的机器 Mi 实现了执行程序 Pj 的机器 Mj 的相同算法，那么只有当解释 Mi 和 Mj 的抽象机器处于双模拟关系时，它们才是相等的。

3.3 非正式方法

Vardi (2012)强调，尽管有许多正式和非正式的定义，但关于算法是什么并没有一致的共识。Gurevich (2000)和 Moschovakis (2001)的方法甚至可以被证明在逻辑上是等价的，但它们只提供了算法的逻辑构造，未能回答主要问题。Hill (2013)建议，对算法的非正式定义，考虑到人们对算法的直观理解，可能更有用，特别是对于公共讨论和从业者与用户之间的沟通。

Rapaport (2012, 附录) 提供了一种尝试总结上述三种经典算法定义的方法，指出：

一个算法（用于执行者 E 完成目标 G）是：

1. 一个过程，即一组有限的语句（或序列）（或规则，或指令），使得每个语句都是：

2. 由有限字母表中的有限数量符号（或标记）组成

3. 并且对于 E 是清晰且明确的

   1. E 知道如何做

   2. 我们可以做到

   3. 它可以在有限的时间内完成

   4. 并且，在这样做之后，E 知道接下来该做什么—

Rapaport 强调算法是一个过程，即一系列有限的陈述，采用规则或说明的形式。有限性在这里通过要求说明包含来自有限字母表的有限数量的符号来表达。

Hill (2016)旨在从 Rapaport（2012）的角度提供算法的非正式定义：

算法是一个有限的、抽象的、有效的、复合的控制结构，是根据特定条件明确给出的，以实现特定目的的。(Hill 2016: 48)。

首先，算法是复合结构，而不是原子对象，即它们由较小的单位组成，即计算步骤。这些结构是有限的和有效的，正如马尔可夫、克林和克努斯明确提到的那样。虽然这些作者没有明确提到抽象性，但希尔（2016）认为这在他们的分析中是隐含的。算法之所以是抽象的，仅仅是因为它们缺乏时空属性，并且独立于它们的实例。它们提供控制，即“通过变量的值和随后的行动表达的，导致从一种状态到另一种状态的某种变化的内容”（第 45 页）。算法是命令式给定的，因为它们命令状态转换以执行指定的操作。最后，算法操作以在通常规定的条件或前提下实现某些目的。从这个观点出发，作者认为，算法在指定一种目标并在某些资源下实现目标方面与规范是相当的。这个定义允许区分算法与其他复合控制结构。例如，食谱不是算法，因为它们不是有效的；游戏也不是算法，因为它们不是命令式给定的。

4. 程序

计算机程序的本体论与计算系统的包容性质密切相关（见 §1）。如果计算系统基于软件-硬件二分法定义，那么程序是解释前者并与硬件的具体性相对立的抽象实体。在 §1.1 中提供了这种解释的示例，包括 Colburn（2000）提出的“具体抽象”定义，Irmak（2012）提出的“抽象工件”特征，以及 Duncan（2011）提出的将程序视为机器规范的观点。相比之下，在 LoAs 的层次结构解释计算系统的情况下，程序是算法的实现。我们参考 §5 对这种意义上程序本体论的分析。本节关注文献中具有重要意义的程序定义，即那些将程序视为理论或工件的观点，重点放在程序与世界之间关系的问题上。

4.1 程序作为理论

程序即理论的观点可以追溯到认知科学的方法。在所谓的信息处理心理学（IPP）的背景下，Newell 和 Simon（1972）提出了这样一个论点：模拟程序是其所模拟系统的经验理论。Newell 和 Simon 将计算机程序赋予了模拟系统的理论角色，同时也赋予了运行该程序的模拟系统（即机器）的角色，以便对模拟系统进行预测。特别是，给定要解决的特定问题时，模拟程序的执行轨迹被用来预测当要求人类主体完成相同任务时将执行的心理操作策略。如果模拟程序的执行轨迹与人类主体的操作策略的口头报告不符，则通过修订模拟程序提供的经验理论。根据 Newell 和 Simon 的说法，这种计算机程序的预测使用类似于通过微分方程或差分方程表达的系统的演化规律的预测使用。

Newell 和 Simon 认为程序就是理论的观点得到了认知科学家 Pylyshyn (1984) 和 Johnson-Laird (1988) 的认同。两者都认为，与典型理论相比，程序更擅长面对需要建模的模拟过程的复杂性，迫使人填补执行程序所需的所有细节。尽管在科学研究的某个阶段可能提出不完整或不连贯的理论，但对于程序来说并非如此。

另一方面，Moore (1978) 认为“程序即理论”论题是计算机科学的另一个神话。由于程序只能模拟某些经验现象的集合，最多只能扮演这些现象的计算模型的角色。Moore 指出，要让程序被认可为模型，仍然需要语义函数来解释被模拟的经验系统。然而，认为程序是模型不应被误解为将程序定义为理论：理论解释和预测模型模拟的经验现象，而程序的模拟并不提供这一点。

根据计算机科学家 Paul Thagard（1984）的观点，将程序理解为理论需要对理论进行句法或语义视图（参见科学理论结构条目）。但程序不符合这两种观点。根据句法观点（Carnap 1966，Hempel 1970），理论是一组用某种定义的语言表达的句子，能够描述目标经验系统；其中一些句子定义了理论的公理，而一些是表达这些系统规律性的类似法则的陈述。程序是一组用某种定义的编程语言编写的指令集，然而，它们并不描述任何系统，因为它们是过程性语言实体而不是声明性语言实体。对此，Rapaport（2020，参见其他互联网资源）反对说，过程式编程语言通常可以转换为声明性语言，并且有一些语言，比如 Prolog，可以同时以过程式和声明式方式解释。根据语义观点（Suppe 1989，Van Fraassen 1980），理论是由一组模型引入的，这些模型被定义为满足理论句子的集合论结构。然而，与 Moore（1978）相反，Thagard（1984）否认程序具有模型的认识论地位：程序模拟物理系统，而不满足理论的法则和公理。相反，程序包括用于模拟目标系统的实现细节，但不包括目标系统的实现细节。

一种不同的方法来解决程序是否是理论的问题来自计算机科学家彼得·诺尔（1985 年）。根据诺尔的观点，编程是一个理论建构过程，不是因为程序本身是理论，而是因为成功程序的开发和生命周期需要程序员和开发人员掌握关于程序的理论。这里所说的理论是按照赖尔（2009 年）的理解，是科学界关于某一组经验现象的知识体系，不一定是公理化或正式表达的。在程序的生命周期中，程序的理论是必要的，以便能够根据观察到的计算错误或对程序被要求解决的计算问题的不满意解决方案的请求来管理程序修改。特别是，程序的理论应该允许开发人员修改程序，以便提供问题的新解决方案。因此，诺尔（1985 年）认为这些理论在软件开发中比文档和规范更为基础。

对于 Turner (2010, 2018 ch. 10) 来说，编程语言是由形式语法和形式语义定义的数学对象。特别地，每个句法构造，比如赋值、条件或循环，都由一个语法规则确定其语法，以及由一个语义规则将意义与之关联。根据是偏好操作语义还是指称语义，意义分别以抽象机器的操作或从状态集到状态集的数学偏函数的形式给出。例如，简单的赋值语句 x:=E 在操作语义下，与机器操作 update(s,x,v) 相关联，该操作将将变量 v 解释为 E 赋给状态 s 中的变量 x。无论是操作语义还是指称语义，程序都可以被理解为表达实现机器操作的数学理论。考虑操作语义：形式为 ⟨P,s⟩⇓s′ 的句法规则在语义上陈述了程序 P 在状态 s 中执行的结果是 s′。根据 Turner (2010, 2018) 的观点，具有操作语义的编程语言类似于一个关于操作的公理化理论，其中规则为关系 ⇓ 提供了公理。

4.2 程序作为技术工件

程序可以被理解为技术工件，因为编程语言的定义，就像其他工件一样，基于功能和结构属性（Turner 2014, 2018 ch. 5）。（高级）编程语言的功能属性由与语言的每个句法构造相关联的语义提供。Turner（2014）指出，只有在其功能层次被孤立时，编程语言才能被理解为公理化理论。另一方面，结构属性是以语言的实现方式来指定的，但并不与计算机的物理组件相对应：给定一个语言的句法构造和相关的功能描述，其结构属性由机器执行的物理操作来确定，以实现对该构造的指令。例如，赋值构造 x:=E 应与表达式 E 的值的物理计算以及将 E 的值放置在物理位置 x 相关联。

编程语言被视为技术工件的另一个要求是，它必须具有赋予语言实现正确性标准的语义。程序员通过将语义视为对程序具有正确性管辖权来证明程序的功能和结构特性。

4.3 程序及其与世界的关系

计算机程序是否是理论的问题与程序与外部世界之间的关系密切相关。如果程序是理论，它们将必须代表某种经验系统，并且程序与世界之间将直接建立语义关系。相比之下，一些人认为程序与自然系统之间的关系是通过外部世界的模型来中介的（Colburn 等人，1993 年，Smith，1985 年）。特别是，Smith（1985 年）认为模型是对经验系统的抽象描述，而在其中运行的计算系统具有充当模型的程序，即它们代表现实的抽象模型。当描述计算机科学中的正确性问题时（见第 7 节），这种关于程序本体论的解释非常有用：如果规范被视为需要计算系统表现出某些行为的模型，那么程序可以被看作是满足规范的模型。

根据是否承认程序与世界的关系，可以提出两种程序观点（Rapaport 2020，第 17 章，参见其他互联网资源）。根据第一种观点，程序是“广义的”、“外部的”和“语义的”：它们直接参照经验系统的对象以及对这些对象的操作。根据第二种观点，程序是“狭义的”、“内部的”和“句法的”：它们仅参照执行计算的实现机器的原子操作。Rapaport（2020，参见其他互联网资源）认为程序不必是“外部的”和“语义的”。首先，计算本身不需要是“外部的”：图灵机通过使用写在磁带上的数据执行其有限表中包含的指令，并在计算产生的数据被写入磁带后停止。数据严格来说并不是从外部用户输入和输出的。此外，Knuth（1973）要求算法具有零个或多个输入和输出（见 § 3.1）。一个不需要输入的计算机程序可能是一个程序，比如输出从 1 开始的所有质数；而一个没有输出的程序可以是一个计算给定变量 x 的值而不返回存储在 x 中的值作为输出的程序。其次，程序不需要是“外部的”、目的论的，即目标导向的。这种观点与文献中其他已知立场相悖。Suber（1988）认为，如果不考虑目标和目的，就不可能评估计算机程序是否正确，也就是说，它是否按照预期行为。正如在 §3.3 中提到的，Hill（2016）在她的非正式定义中指出，算法实现“在给定条件下达到给定目的”。对于这些观点，Rapaport（2020，第 17 章，参见其他互联网资源）回应说，虽然目标、目的和程序员的意图对于人类计算机理解程序可能非常有用，但对于人工计算机执行程序代码指示的计算来说并非必要。事实上，古典方法要求算法具有的有效性原则（见 §3.1）要求算法在没有任何直觉的情况下执行。换句话说，执行加法自然数程序的机器并不“理解”它正在进行加法；同时，知道给定程序执行加法可能有助于人类理解程序的代码。

根据这一观点，计算仅涉及符号，而非含义。 图灵机成为符号操作者，其操作可以关联不止一个意义。那么，如果不通过它们的含义，即考虑它们执行的功能，如何确定两个程序是相同的程序呢？一个答案来自皮奇尼（Piccini）对计算及其“内部语义”（Piccini 2008 年，2015 年第 3 章）的分析：通过仅分析它们的语法和程序对符号执行的操作，可以将两个程序确定为相同。字符串操作的效果可以被视为程序的内部语义。后者可以通过隔离程序代码中的子程序或方法轻松确定，并随后用于识别一个程序或确定两个程序是否相同，即当它们由相同的子程序定义时。

然而，有人认为存在这样的情况，即在没有参考外部语义的情况下无法确定两个程序是否相同。Sprevak (2010) 提出考虑两个执行加法的程序，其中一个操作阿拉伯数字，另一个操作罗马数字。这两个程序计算相同的函数，即加法，但不能仅通过检查带有子程序的代码来确定这一点；必须通过为输入/输出字符串分配内容，将阿拉伯数字和罗马数字解释为数字来确定。在这方面，Angius 和 Primiero (2018) 强调计算机程序的身份问题与自然种类 (Lowe 1998) 和技术制品 (Carrara 等人 2014) 的身份问题并无不同。这个问题可以通过确定一个身份标准来解决，即一个形式关系，任何两个程序都应该遵守这个关系才能被定义为相同。Angius 和 Primiero (2018) 展示了如何使用过程代数之间的双模拟关系作为两个程序实现的两个自动机之间的身份标准。双模拟允许建立实现相同函数的程序的匹配结构属性，同时提供了关于模拟的更弱副本标准。这将讨论重新引向程序作为实现的概念。我们现在转向分析这个后一概念。

5. 实施

‘实现’一词通常与计算系统的物理实现相关联，即指机器执行计算机程序。特别是根据第 1.1 节中考察的计算系统的双重本体论，这种意义上的实现归结为结构硬件，而非功能软件。相比之下，遵循抽象层次方法（第 1.2 节），实现变成了一个更广泛的关系，它存在于定义计算系统的任何抽象层次和层次结构更高的之间。因此，算法是（一组）规范的实现；用高级编程语言表达的程序可以被定义为算法的实现（见第 4 节）；汇编和机器码指令可以被视为相对于给定 ISA 的一组高级编程语言指令的实现；最后，执行是那些机器码指令的物理、可观察的实现。同样地，用高级语言制定的程序也是规范的实现，并且正如双重本体论范式所主张的那样，执行是高级编程语言指令的实现。根据 Turner（2018）的观点，甚至规范也可以被理解为所谓意图的实现。

这里需要进一步审查的是因此定义的实现关系的性质。分析这种关系对于定义正确性概念至关重要（§7）。确实，一个正确的程序等同于一个算法的正确实现；一个正确的计算系统是一组规范的正确实现。换句话说，在这种观点下，正确性概念与实现概念相配对，对于任何层次（LoA）：只有当某个层次是其正确实现时，才能说任何层次相对于更高层次是正确的。

以下三个小节考察了在计算机科学哲学文献中提出的三种主要实现关系的定义。

5.1 实现作为语义解释

计算机科学中对实现概念的首次哲学分析是由 Rapaport（1999 年，2005 年）提出的。他将实现 I 定义为在实现媒介 M 中对句法或抽象域 A 的语义解释。如果将实现理解为在计算系统的层次本体论中给定的 LoA 与任何上层之间的关系，那么 Rapaport 的定义相应地得到扩展，以便任何 LoA 为上层提供在给定实现媒介中的语义解释。在这种观点下，规范提供了对利益相关者在规范（形式）语言中表达的意图的语义解释，而算法则使用算法可以用自然语言、伪代码、逻辑语言、函数式语言等之一来表达规范的语义解释。实现媒介可以是抽象的或具体的。计算机程序是算法的实现，因为前者在高级编程语言中提供了对后者的句法构造的语义解释作为其实现媒介。程序的指令在编程语言中解释算法的任务。此外，执行 LoA 将汇编/机器代码操作的语义解释转换为由物理机器的结构特性给定的媒介。根据 Rapaport（1999 年，2005 年）的分析，实现是一种非对称关系：如果 I 是 A 的实现，那么 A 不能是 I 的实现。然而，作者认为任何 LoA 既可以是句法级别，也可以是语义级别，即它既可以扮演实现 I 的角色，也可以扮演句法域 A 的角色。虽然算法通过用高级语言表达的程序被赋予语义解释，但同一算法也为规范提供了语义解释。由此可见，抽象-实现关系将计算系统的功能-结构关系配对。

Primiero (2020) 认为这后一方面是 Rapaport（1999, 2005）关于实现的主要限制之一：实现被简化为一个句法层与其语义解释之间的唯一关系，并且没有考虑到计算系统在第 1.2 节中所见的分层本体论。为了将当前的实现定义扩展到所有 LoAs，每个层次都必须每次重新解释，无论是作为句法层还是语义层。这反过来又对第二个困难产生了影响，根据 Primero (2020) 的说法，将实现视为语义解释：一方面，这种方法没有考虑不正确的实现；另一方面，对于给定的不正确实现，如此定义的唯一关系只能将不正确性与一个句法层联系起来，排除所有其他层次作为潜在错误位置。

Turner (2018) 的目标是表明语义解释不仅不能解释错误的实现，甚至不能解释正确的实现。第一个例子是通过将一种语言实现到另一种语言来提供的：这里的实现语言并没有为被实现语言提供语义解释，除非前者与为后者提供意义和正确性标准的语义相关联。这样的语义将保持在实现关系之外：虽然正确性与语义解释相关联，但实现并不总是伴随着语义解释。第二个例子是通过考虑由数组实现的抽象堆栈来给出的；同样，数组并没有为堆栈提供正确性标准。相反，堆栈规定了其任何实现（包括数组在内）的正确性标准。

5.2 实现作为关系规范-工件

提供实现关系的正确性标准的事实是由抽象层次引起的，这促使 Turner (2012, 2014, 2018) 将实现定义为关系规范-工件。正如在 §2 中所检验的那样，规范对工件具有正确性管辖权，即规定了工件的允许行为。还要记住，工件可以是抽象的也可以是具体的实体，并且任何 LoA 都可以作为较低层次的规范。这意味着规范-工件关系能够定义计算系统分层本体论中的任何实现关系。

根据规范-工件关系的定义方式，Turner (2012) 区分了多达三种不同的实现概念。考虑一个物理机器实现给定抽象机器的情况。根据一种意向性实现概念，抽象机器作为物理机器的规范，只要它推进了后者必须满足的所有功能要求，即它原则上指定了实现物理机器的所有允许行为。根据一种外延性实现概念，只有当可以建立将后者的状态映射到前者状态的同构时，物理机器才是抽象机器的正确实现，并且抽象机器中的转换对应于工件的实际执行（计算痕迹）。最后，一种经验性实现概念要求物理机器展示与抽象机器规定的计算相匹配的计算；换句话说，正确的实现必须通过测试经验地进行评估。

Primiero (2020) 强调，尽管这种方法解决了正确性和错误计算的问题，因为它允许区分正确和不正确的实现，但仍然确定了规范级别和工件级别之间的唯一实现关系。再次，如果允许此解释涉及计算系统的分层本体论，通过重新解释每个 LoA，无论是规范还是工件，Turner 的解释都阻止了将多个级别同时作为错误计算的原因：错误计算总是发生在工件对规范的不正确实现上。通过将实现定义为跨越所有 LoAs 的关系，人们将能够识别多个不正确的实现，这些实现不直接参考抽象规范。错误计算确实可能是由于较低级别的不正确实现而导致，然后一直继承到执行级别。

5.3 用于 LoAs 的实现

Primiero (2020) 提出了一种对实现的定义，不是作为两个固定层次之间的关系，而是允许在任何抽象层次上变化的关系。在这种观点下，一个实现 I 是一个实例化关系，它在抽象层次结构中连接一个层次和任何更高的层次。因此，一个物理计算机是汇编/机器码操作的实现；通过传递性，它也可以被视为高级编程语言指令集的实例化。用高级语言表达的程序是算法的实现；但它也可以被看作是一组规范的实例化。

这样对实现的定义使 Primiero (2020)能够提供正确性的一般定义：如果一个物理计算系统在任何 LoA 上都具有正确的实现，那么它就是正确的。因此，正确性和实现在任何 LoA 上都是耦合的，并且被定义。功能正确性是计算系统的属性，显示出该系统规范要求的功能。过程正确性表征显示出实现算法所需功能的计算系统。执行正确性被定义为系统能够在其体系结构上正确执行程序的属性。这些正确性形式中的每一种也可以根据满足的功能数量进行定量分类。功能高效的计算系统显示出规范要求的功能的最小子集；功能最优系统能够显示出这些功能的最大子集。同样，作者定义了过程和执行高效以及最优的计算系统。

5.4 物理计算

根据这一定义，实现从一个层次转移到另一个层次：定义计算系统的一组算法被实现为某种形式语言中的过程，高级语言中的指令，或低级编程语言中的操作。一个有趣的问题是，除了计算工件之外，是否实现这种类型程序的任何系统都可以被视为计算系统。换句话说，询问物理实现的本质实际上是在询问什么是计算系统。如果任何实现算法的系统都可以被视为计算系统，那么这类系统的范围可以扩展到生物系统，如大脑或细胞；物理系统，包括宇宙或其某部分；最终扩展到任何系统，这是一种被称为泛计算主义的论点（有关该主题的详尽概述，请参阅 Rapaport，2018 年）。

传统上，计算系统被理解为一种机械装置，接受输入数据，根据一组指令进行算法处理，然后将处理后的数据作为输出返回。例如，冯·诺伊曼（1945 年，第 1 页）指出：“自动计算系统是一种（通常是高度复合的）设备，可以执行指令以进行相当复杂的计算”。这样一种非正式且广泛接受的定义留下了一些问题，包括计算系统是否必须是机器，它们是否必须按算法处理数据，因此计算是否必须是图灵完备的。

Rapaport (2018) 提供了对计算系统的更明确描述，定义为任何“物理上合理的实现，逻辑上等价于通用图灵机的任何东西”。严格来说，个人计算机并不是物理图灵机，但寄存器机已知是图灵等价的。为了被视为计算系统，系统必须是其合理的实现，因为与物理机器相反，图灵机可以访问无限的内存空间，并且作为抽象机器，是无错误的。根据 Rapaport（2018）的定义，这种类型的任何物理实现都是计算系统，包括自然系统。这引发了一个问题，即哪类自然系统能够实现图灵等价的计算。西尔尔（Searle）曾经著名地主张任何东西都可以是图灵机的实现，或者是逻辑等价模型的实现（Searle，1990）。他的论点基于图灵机是一种句法属性，即一切都是关于操纵 0 和 1 的标记。根据西尔尔的观点，句法属性并不是物理系统的固有属性，而是由观察者赋予给它们的。换句话说，系统的物理状态并非固有地是计算状态：必须有一个观察者或用户，将该状态赋予一个计算角色。由此可见，任何行为可以描述为 0 和 1 的句法操作的系统都是计算系统。

Hayes (1997) 反对 Searle (1990) 的观点，即如果一切都是计算系统，那么属性“作为计算系统”将变得无意义，因为所有实体都将具备这一属性。相反，存在一些是计算系统的实体，也存在一些不是的实体。计算系统是那些能够改变自身接收的模式并保存到内存中的实体。换句话说，Hayes 指出存储的输入既可以是数据也可以是指令，并且指令在执行时能够修改某些输入数据的值。“如果它是纸，那就是‘魔法纸’，上面的文字可能会自发改变，或者出现新的文字” (Hayes 1997, p. 393)。只有能够像“魔法纸”一样运作的系统才能被认定为计算系统。

一种不同的方法来自皮奇尼尼（2007 年，2008 年），在他对物理计算的机械分析中（皮奇尼尼 2015 年；另请参阅物理系统中计算的条目）。物理计算系统是一个系统，其行为可以通过描述带来这些行为的计算机制来机械地解释。机制可以被定义为“实体和活动组织在一起，以便它们从开始或设置到完成或终止条件产生规律性变化”（Machamer 等人 2000 年；请参阅科学中机制的条目）。作为物理过程的计算可以被理解为那些“根据适用于所有输入字符串的一般规则以及取决于输入（有时是内部状态）生成输出字符串的机制”（皮奇尼尼 2007 年，第 108 页）。很容易确定计算过程的设置和终止条件。任何可以通过描述基础计算机制来解释的系统都应被视为计算系统。对解释的关注帮助皮奇尼尼避免了西尔的结论，即任何系统都是计算系统：即使原则上可以将任何给定的实体和活动集解释为计算机制，但只有需要通过计算机制来解释某种观察到的现象才能将正在检查的系统定义为计算系统。

6. 验证

软件开发过程中的一个关键步骤是验证。这包括评估给定计算系统是否符合其设计规范的过程。在计算机行业的早期阶段，有效性和正确性检查方法包括几种设计和构建技术，例如（Arif 等，2018）。如今，正确性评估方法大致可以分为两大类：形式验证和测试。形式验证（Monin 和 Hinchey，2003）涉及使用数学工具证明正确性；软件测试（Ammann 和 Offutt，2008）则是运行实现的程序，观察执行是否符合高级规范。在许多实际情况下，通常会结合使用这两种方法（例如参见 Callahan 等，1996）。

6.1 模型和理论

形式验证方法需要对待验证软件进行表示。在定理证明中（见 van Leeuwen 1990），程序以公理系统和表示程序转换的前置条件和后置条件的推理规则的形式表示。然后，通过从公理中推导表达规范的公式来获得正确性证明。在模型检验中（Baier 和 Katoen 2008），程序以状态转换系统的形式表示，其属性规范通过时间逻辑公式（Kröger 和 Merz 2008）形式化，通过深度优先搜索算法实现正确性证明，检查这些公式是否适用于状态转换系统。

用于正确性评估的公理系统和状态转换系统可以被理解为所代表物件的理论，因为它们被用来预测和解释它们的未来行为。方法论上，模型检验中的状态转换系统可以与经验科学中的科学模型进行比较（Angius 和 Tamburrini，2011）。例如，Kripke 结构（见 Clarke 等人，1999 年第 2 章）符合 Suppes（1960）对科学模型的定义，即作为建立与通过对目标经验系统进行实验收集的数据模型的适当映射关系的集合论结构（另请参见科学模型条目）。Kripke 结构和其他在形式验证方法中使用的状态转换系统通常被称为系统规范。它们与常规规范（也称为属性规范）有所区别。后者指定了编码程序必须实例化的一些所需行为属性，而前者指定（原则上）已编码程序的所有潜在执行，从而允许对其轨迹进行算法检查（Clarke 等人，1999 年）。为了实现这一目标，系统规范被视为假设结构，根据程序代码和允许的状态转换，假设目标计算系统的潜在执行集（Angius，2013b）。事实上，一旦检查了某个时态逻辑公式是否符合建模的 Kripke 结构，就会对所代表的程序针对与所检查公式对应的行为属性进行经验测试，以评估模型假设是否是目标计算系统的充分代表。因此，属性规范和系统规范在其故意立场上也有所不同（Turner，2011）：前者是对要编码的程序的要求，而后者是对编码程序的（假设性）描述。在模型检验中，状态转换系统的描述性和假设性特征是将状态转换系统与科学模型并列的另一个重要特征。

6.2 测试和实验

测试是启动程序并观察其执行过程以评估其是否符合提供的属性规范的更“经验主义”的过程。这种技术在软件开发过程中被广泛使用。哲学家和具有哲学思维的计算机科学家已经考虑了软件测试在科学发现传统方法论的光线下（Snelting 1998; Gagliardi 2007; Northover 等，2008; Angius 2014），并质疑软件测试是否可以被视为评估程序正确性的科学实验（Schiaffonati 和 Verdicchio 2014，Schiaffonati 2015; Tedre 2015）。

Dijkstra（1970 年，第 7 页）提出的著名格言“程序测试可以用来显示错误的存在，但永远不能用来显示错误的不存在”，将 Popper（1959 年）的可证伪性原则引入了计算机科学（Snelting，1998）。针对给定时间间隔的高级属性规范测试程序可能会出现一些故障，但如果在观察运行程序时没有发生故障，就不能得出程序是正确的结论。下一次系统运行可能会观察到不正确的执行。原因在于测试人员只能使用潜在程序输入集的有限子集启动程序，并且只能在有限时间间隔内进行测试；因此，无法经验观察到待测试程序的所有潜在执行。因此，软件测试的目的是检测程序的错误，而不是保证其不存在（Ammann 和 Offutt，2008 年，第 11 页）。程序是可证伪的，因为测试可以揭示错误（Northover 等，2008 年）。因此，鉴于计算系统和属性规范，测试类似于科学实验，通过观察系统行为，试图证伪程序相对于感兴趣的规范是正确的假设。

然而，科学实验的其他方法论和认识论特征并不适用于软件测试。第一个方法论区别在于，一个证伪测试导致计算系统的修订，而不是像测试科学假设那样修订假设。这是由于科学中规范和经验假设的故意立场的差异（Turner 2011）。规范是要求，其违反要求进行程序修订，直到程序成为规范的正确实例。

基于这一原因以及其他原因，传统的科学实验概念需要被“延伸”，以便应用于软件测试活动（Schiaffonati 2015）。以理论驱动为特征的实验，构成了大部分实验科学，而这在实际计算机科学实践中并没有对应物。如果排除了测试与形式方法相结合的情况，那么软件工程师进行的大部分实验都是探索性的，即旨在“探索”“关于工件功能及其与环境交互的可能性领域，在没有适当理论或理论背景的情况下”（Schiaffonati 2015: 662）。软件测试人员通常无法对他们进行的实验进行理论控制；对计算系统与用户及环境互动行为的探索允许测试人员对观察到的行为进行理论概括。计算机科学中的探索性实验还表现为程序经常在类似真实环境中进行测试，测试人员扮演用户的角色。然而，理论驱动实验的一个重要特征是实验者不参与即将进行的实验。

因此，虽然一些软件测试活动更接近于实证科学中的实验活动，但另一些则定义了一种属于软件开发过程的新实验类型。在指定、实施和评估计算系统的过程中可以区分出五种实验类型（Tedre，2015 年）：

• 进行可行性实验以评估系统是否执行用户和利益相关者指定的功能

• 进行试验实验以评估系统在一组初始条件下的独立能力；

• 在真实环境中进行田间实验，而不是在模拟环境中进行

• 比较实验测试类似系统，在不同方式实例化相同功能，以评估哪种实例化在类似真实和真实环境中更好地执行所需功能;

• 最后，控制实验被用来评估对测试计算系统行为的先进假设，它们是与科学理论驱动实验相媲美的唯一实验，因为它们是基于某些正在评估的理论假设进行的。

6.3 解释

软件测试被认为是成功的，当检测到误差时（假设没有计算工件是 100%正确）。接下来的步骤是找出导致执行不正确的原因，即追溯故障（更熟悉地称为“bug”），然后进行调试阶段，再次测试系统。换句话说，需要提出对观察到的误差计算的解释。

已经做出了努力来考虑计算机科学中的解释（Piccinini 2007; Piccinini and Craver 2011; Piccinini 2015; Angius and Tamburrini 2016）与科学哲学中不同解释模型的关系。特别是，计算解释可以被理解为一种特定类型的机械解释（Glennan 1996; Machamer et al. 2000; Bechtel and Abrahamsen 2005），因为计算过程可以被分析为机制（Piccinini 2007; 2015; 另请参阅物理系统中计算的条目）。

考虑一个执行指令的处理器。所涉及的过程可以被理解为一个机制，其组成部分是处理器中实例化相关硬件规格（寄存器规格，算术逻辑单元等）所规定功能的状态和组合元素，这些元素被组织在一起，以便能够执行观察到的执行。提供这种机制的描述被视为推进对观察到的计算的机械解释，比如对操作故障的解释。

对于每一种误计算类型（见 §7.3），都可以在适当的 LoA 上定义相应的机械解释，并针对表征该 LoA 的规范集。事实上，机制的抽象描述仍然以机械解释的形式提供给人们，这种形式被定义为“一个可以填充已知组件部分和活动描述的机制模式的截断抽象描述”（Machamer 等人，2000 年，第 15 页）。例如，假设一个非常常见的情况，即机器通过执行包含语法错误的程序（称为滑动）而误计算。计算机无法正确实现程序规范提供的功能要求。然而，为了解释的目的，在硬件抽象层面提供发生的滑动的解释，通过推进硬件组件的详细描述及其功能组织，这将是多余的。在这种情况下，一个令人满意的解释可能在于展示程序代码不是提供的程序规范的正确实例化（Angius 和 Tamburrini，2016）。为了机械地解释发生的误计算，提供错误程序的描述可能就足够了，抽象出计算机机制的其余部分（Piccinini 和 Craver，2011）。抽象不仅是软件开发和规范中的优点，也是计算系统行为解释中的优点。

7. 正确性

在前一节中审查的软件验证的不同方法中，每种方法都假定对软件正确性有不同的理解。通常，正确性被理解为抽象与其实现之间的关系，即当后者满足前者制定的属性时，该关系成立。一旦计算系统被描述为具有分层本体论，正确性就需要重新制定为任何结构层与其功能层之间的关系（Primiero, 2020）。因此，当在抽象和功能层之间制定时，正确性仍然可以被视为数学关系；而当在功能和实现层之间制定时，可以被视为经验关系。计算机科学哲学中早期的一场辩论（De Millo 等，1979 年；Fetzer，1988 年）确实围绕着这一区别展开。

7.1 数学正确性

形式验证方法授予程序行为的先验分析，无需观察其任何实现或考虑其执行。特别是，定理证明允许推断所考虑程序的任何潜在行为及其行为特性，从适当的公理表示中。在模型检查的情况下，通过在给定集合论模型中执行算法搜索有效的公式，可以预先了解程序执行显示的行为特性。这些考虑使霍尔（1969）著名地得出结论，即程序开发是一门“精确科学”，应以正确性的数学证明为特征，在认识论上与数学实践中的标准证明相媲美。

De Millo 等人（1979）质疑霍尔（Hoare）的论点：正确的数学证明通常是优雅且易于理解的，这意味着任何（专家）读者都可以“看到”结论是如何从前提中得出的（关于软件优雅性的概念，也请参见 Hill（2018））。通常被称为笛卡尔证明（Hacking，2014）的证明在正确性证明中没有对应物，通常冗长而繁琐，难以理解，也没有解释为什么结论必然从前提中得出。然而，数学中的许多证明是冗长且复杂的，但它们原则上是可以调查的，这要归功于引理、抽象和逐步引导到待证陈述的新概念的分析构造。相反，正确性证明不涉及新概念的创造，也不涉及数学证明中通常发现的模块化（Turner，2018）。然而，不可调查的证明不能被视为数学证明（Wittgenstein，1956）。

关于计算机程序正确性证明的第二个理论困难涉及其复杂性以及待验证程序的复杂性。Hoare（1981）已经承认，虽然原则上验证正确性是可能的，但在实践中几乎是难以实现的。除了琐碎的情况外，当代软件是模块化编码的，需要满足大量的规范，并且被开发为与其他程序、系统、用户进行交互。嵌入式和反应式软件就是一个例子。为了验证这样复杂的软件，正确性证明是自动进行的。因此，一方面，正确性问题从正在检查的程序转移到执行验证的程序，例如定理证明器；另一方面，由物理过程进行的证明可能出错，这是由于机器的机械错误。针对这种无限回归论证，Arkoudas 和 Bringsjord（2007）认为，可以利用证明检查器，因为它是一个相对较小的程序，通常更容易验证。

最近，基于逻辑和统计分析相结合的形式化方法为这一研究领域注入了新的动力：分离逻辑（Reynolds, 2002）能够提供对计算系统物理内存的逻辑行为的表示，同时考虑输入的概率分布作为错误的统计来源的可能性，使得能够对像 Facebook 平台这样的大型交互系统进行形式化正确性检查成为可能（另见 Pym 等人，2019）。

7.2 物理正确性

Fetzer (1988) 反对认为，演绎推理只能保证程序相对于其规范的正确性，但不能保证计算系统的正确性，因为计算系统还考虑了程序的物理实现。即使程序相对于任何相关的上层 LoAs（算法、规范、需求）是正确的，但由于物理故障，其实现仍可能违反一个或多个预期规范。前一种正确性原则上可以在数学上证明，但执行 LoA 的正确性需要经验评估。正如第 6.2 节所述，软件测试原则上只能显示计算系统的正确性。在实践中，非平凡系统的允许执行次数可能是无限的，并且无法在有限（或合理）的时间内进行详尽检查（Dijkstra 1974）。大多数成功的测试方法更倾向于同时使用形式验证和测试，以达到令人满意的纠正水平。

对于数学正确性的理论可能性的另一个异议是，由于证明是由定理证明器（即物理机器）执行的，所以人们对计算系统的知识不是先验的，而是经验的（参见 Turner 2018 第 25 章）。然而，Burge（1988）认为，基于计算机的正确性证明仍然可以被视为先验的，即使它们的可能性取决于感官经验，但它们的证明并不是（就像后验知识一样）。例如，红色是一种颜色的知识是先验的，即使它需要对红色进行感官体验；这是因为“红色是一种颜色”是真实的，独立于任何感官经验。有关计算机在数学证明中使用性质的进一步讨论，请参见（Hales 2008；Harrison 2008；Tymoczko 1979，1980）。

正确性问题最终归结为询问物理机器如何满足抽象要求的含义。根据简单映射理论，计算系统 S 只有在以下情况下才是规范 SP 的正确实现：

1. 可以从 S 赋予的状态到由 SP 定义的状态建立一个同态映射，

2. 对于状态空间 S 中的任何状态转移 s1→s2，都存在状态空间 SP 中的状态转移 s′1→s′2，其中状态 s′1 映射到 s1，状态 s′2 映射到 s2。

简单映射解释只要求 S 和 SP 的描述在外延上达成一致。这种解释的弱点在于很容易确定任何一对物理系统规范之间的外延一致，为泛计算主义观点留下了空间。

对于泛计算论的危险性使一些作者试图对正确实施进行解释，从某种程度上限制了可能解释的类别。特别是，

1. 因果解释（D. J. Chalmers 1996; Copeland 1996）表明，物质条件句（如果系统处于物理状态 s1 ...）被替换为反事实条件句。

2. 语义学观点认为，计算系统必须与语义描述相关联，指定系统要实现什么（Sprevak 2012）。例如，一个物理设备可以被解释为一个与门或一个或门，但如果没有设备的定义，就无法确定这个工件是什么。

3. 该句法解释要求只有可以定义为句法的物理状态才能映射到计算状态。尚待审查的是什么定义了一个句法状态（请参阅 Piccinini 2015 年或物理系统中关于计算的条目以获取句法解释的概述）。

4. 规范解释（Turner 2012）认为，不仅抽象和物理计算过程必须一致，而且抽象规范对系统具有规范力。根据这样的说法，计算是由抽象规范确定功能的物理过程。这种关系比语义解释更强，后者要求简单的描述性关系，也比句法解释更强，后者侧重于句法对象及其语义解释。

7.3 计算错误

根据迄今为止所说的内容，可以得出结论：实现程序的正确性并不能自动确立计算系统的良好运行。 图灵（1950）已经区分了功能错误和结论错误。前者是由于错误的实现而无法执行某些高级语言程序的指令；结论错误表征了正确的抽象机器，但仍未能执行它们应该完成的任务。这可能发生在那些程序正确实例化了某些规范的情况下，这些规范并未正确表达用户对该程序的需求。在这两种情况下，实现正确程序的机器仍然可以说是计算错误。

图灵关于功能错误和结论错误的区分已经被扩展为一种完整的误计算分类学（Fresco 和 Primiero，2013 年）。这种分类是基于定义计算系统的不同 LoAs 建立的。错误可以是：

• 概念上：它们违反了要求在命题合取范式中表达的规范具有一致性的有效性条件；

• 材料：它们违反了关于其规范集的程序正确性要求

• 当物理约束被一些故障的实施硬件所突破时，这些错误就会出现。

可执行错误仅在执行级别明显出现，它们对应于图灵（1950）的功能错误，也称为操作故障。概念和物质错误可能在从意图级别到物理实现级别的任何抽象级别上出现。概念错误会导致错误，而物质错误会导致失败。例如，在意图级别上的错误包括不一致的需求集，而在物理实现级别上，它可能对应于无效的硬件设计（例如，在选择真功能连接的逻辑门时）。在规范级别发生的故障可能是由于设计被认为与所需的功能要求集不完整而导致的，而在算法级别发生的故障发生在那些算法被发现未能满足规范的常见情况中。除了错误、失败和操作故障之外，滑动是高级编程语言指令级别的误计算的来源：它们可能是由于程序中的语法或语义缺陷而导致的概念或物质错误。概念滑动出现在所有违反高级语言的语法规则的情况中；物质滑动涉及违反编程语言的语义规则，例如当使用但未初始化变量时。

需要进一步区分基于软件的计算系统中的功能障碍和误功能（Floridi、Fresco 和 Primiero，2015）。软件只能误功能，但永远不会功能障碍。如果软件令牌的物理实现未能满足意图或规范，则软件令牌可能会功能障碍。功能障碍仅适用于单个令牌，因为令牌功能障碍表现为其在实施功能方面与同一类型的其他令牌的行为不一致。因此，功能障碍不适用于意图级别和规范级别。相反，软件类型和令牌都可能误功能，因为误功能不取决于能否与同一类型的令牌进行比较以执行某些实施功能。令牌的误功能通常取决于其他组件的功能障碍，而类型的误功能通常是由于设计不佳。软件令牌不能功能障碍，因为给定类型的所有令牌都以意图级别和规范级别统一指定的功能进行实现。这些功能在算法实现级别上实现，然后在执行级别上执行；在正确实施的情况下，所有令牌将在执行级别上正确运行（前提是没有操作故障发生）。出于同样的原因，软件令牌不能误功能，因为它们是相同意图和规范的实现。只有在设计不佳的情况下，软件类型才可能误功能；误功能的软件类型能够正确执行其功能，但也可能产生一些不良副作用。有关将故障分类概念应用于恶意软件分类问题，请参见（Primiero 等人，2019）。

8. 计算机科学的认识论地位

在 20 世纪 60 年代和 70 年代之间，计算机科学作为一门独立于其较老的学科兄弟数学和物理的学科出现，随之而来的是定义其认识论地位的问题，受到数学、经验和工程方法的影响（Tedre 和 Sutien，2008 年，Tedre，2011 年，Tedre，2015 年，Primiero，2020 年）。关于计算机科学是否应主要被视为数学学科、工程学分支或科学学科的辩论至今仍在进行中。

8.1 计算机科学作为一门数学学科

任何关于计算机科学的认识论描述都基于本体论、方法论和认识论承诺，即关于计算系统性质、指导软件开发过程的方法以及所涉及的推理类型（演绎、归纳或两者的结合）的假设（Eden 2007）。

计算作为数学概念的分析起源于逻辑，希尔伯特关于谓词演算的可决问题，即所谓的 Entscheidungsproblem（Hilbert 和 Ackermann，1950）：是否存在一种机械过程，可以判断逻辑中的任意句子是否可证明？为了回答这个问题，需要一个严格的模型来描述逻辑和数学中的有效或机械方法的非正式概念。这首先是一个数学努力：必须发展非正式概念的数学类比。认为计算机科学具有数学性质的支持者认为，计算机程序可以被看作是这种数学实体的物理实现，并且可以通过理论计算机科学的形式方法推理程序。Dijkstra（1974）和 Hoare（1986）非常明确地认为程序的指令是数学句子，并且考虑以公理系统为基础的编程语言的形式语义（Hoare，1969）。只要程序规范和指令是用相同的形式语言提出的，形式语义提供了证明正确性的手段。因此，通过数学正确性证明中涉及的演绎推理，可以获得有关计算系统行为的知识。这种理性乐观主义（Eden，2007）的基础是，计算系统是人造系统，因此可以确切地预测它们的行为（Knuth，1974）。

虽然是理论计算机科学的一个核心关注点，但可计算性和复杂性的主题已在现有条目中涵盖了关于哥德尔-图灵论题、计算复杂性理论和递归函数的内容。

8.2 计算机科学作为一门工程学学科

在 20 世纪 70 年代后期，计算系统在日常环境中的应用数量不断增加，随之而来的市场需求激增导致了学术界和工业界计算机科学家兴趣的偏移：从关注证明程序正确性的方法转向关注管理复杂性和评估系统可靠性的方法（Wegner 1976）。事实上，正式表达嵌入在更大系统中并与用户交互的高度复杂程序的规范、结构和输入几乎是不可能的，因此提供它们正确性的数学证明在大多数情况下是不可行的。计算机科学研究朝着能够提供统计正确性评估的测试技术发展，通常称为可靠性（Littlewood 和 Strigini 2000），以估计程序代码中错误分布的方法。

符合计算机科学的工程学观点的是，计算系统的可靠性是以与土木工程评估桥梁和航空航天工程评估飞机相同的方式进行评估的（DeMillo 等人，1979 年）。特别是，尽管实证科学研究存在的是什么，计算机科学侧重于可能存在的是什么，即如何生产工件，并且因此应该被认为是“数学工程”（Hartmanis，1981 年）。同样，尽管科学探究涉及发现有关观察现象的规律，但在计算机科学实践中无法确定适当的规律，因为后者更多地涉及生产涉及计算工件的现象（Brooks，1996 年）。

8.3 计算机科学作为一门科学学科

正如第 6 节所述，由于软件测试和可靠性测量技术以其无法保证代码缺陷不存在而闻名（Dijkstra 1970），在许多情况下，特别是对于评估所谓的安全关键系统（如飞机、火箭、核电厂等的控制器）时，通常会结合形式化方法和经验测试来评估正确性和可靠性。因此，计算机科学可以被理解为一门科学学科，因为它利用了演绎和归纳概率推理来检验计算系统（Denning 等人 1981, 2005, 2007; Tichy 1998; Colburn 2000）。

计算机科学在方法论上与实证科学齐平的论点可以追溯到纽厄尔、佩里斯和西蒙 1967 年在《科学》杂志上的信件（纽厄尔等人，1967 年），并主导了整个 1980 年代（韦格纳，1976 年）。在 1975 年的图灵奖演讲中，纽厄尔和西蒙提出了：

计算机科学是一门经验性学科。我们本来可以称之为实验科学，但像天文学、经济学和地质学一样，它的一些独特的观察和经验形式并不符合实验方法的狭隘刻板印象。尽管如此，它们仍然是实验。每一台新建造的机器都是一个实验。实际上构建这台机器向自然提出了一个问题；我们通过观察机器的运行并利用所有可用的分析和测量手段来分析它，以期倾听自然的回答（Newell 和 Simon，1975 年，第 114 页）。

自从纽厄尔和西蒙的图灵奖演讲以来，计算机科学可以被理解为一种特殊类型的经验科学，这与计算实验的性质有关。事实上，关于计算机科学的认识论地位的许多当前讨论涉及定义它是何种科学的问题（Tedre 2011，Tedre 2015），特别是计算机科学中实验的性质（Schiaffonati 和 Verdicchio 2014），计算中的定律和定理的性质（Hartmanis 1993；Rombach 和 Seelish 2008），以及计算机科学与软件工程之间的方法论关系（Gruner 2011）。

Bibliography

• Abramsky, Samson & Guy McCusker, 1995, “Games and Full Abstraction for the Lazy λ-Calculus”, in D. Kozen (ed.), Tenth Annual IEEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 234–43. doi:10.1109/LICS.1995.523259

• Abramsky, Samson, Pasquale Malacaria, & Radha Jagadeesan, 1994, “Full Abstraction for PCF”, in M. Hagiya & J.C. Mitchell (eds.), Theoretical Aspects of Computer Software: International Symposium TACS ‘94, Sendai, Japan, April 19–22, 1994, Springer-Verlag, pp. 1–15.

• Abrial, Jean-Raymond, 1996, The B-Book: Assigning Programs to Meanings, Cambridge: Cambridge University Press.

• Alama, Jesse, 2015, “The Lambda Calculus”, The Stanford Encyclopedia of Philosophy (Spring 2015 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/spr2015/entries/lambda-calculus/.

• Allen, Robert J., 1997, A Formal Approach to Software Architecture, Ph.D. Thesis, Computer Science, Carnegie Mellon University. Issued as CMU Technical Report CMU-CS-97-144. Allen 1997 available on line

• Ammann, Paul & Jeff Offutt, 2008, Introduction to Software Testing, Cambridge: Cambridge University Press.

• Angius, Nicola, 2013a, “Abstraction and Idealization in the Formal Verification of Software”, Minds and Machines, 23(2): 211–226. doi:10.1007/s11023-012-9289-8

• –––, 2013b, “Model-Based Abductive Reasoning in Automated Software Testing”, Logic Journal of IGPL, 21(6): 931–942. doi:10.1093/jigpal/jzt006

• –––, 2014, “The Problem of Justification of Empirical Hypotheses in Software Testing”, Philosophy & Technology, 27(3): 423–439. doi:10.1007/s13347-014-0159-6

• Angius, N., & Primiero, G., 2018, “The logic of identity and copy for computational artefacts”, Journal of Logic and Computation, 28(6): 1293–1322.

• Angius, Nicola & Guglielmo Tamburrini, 2011, “Scientific Theories of Computational Systems in Model Checking”, Minds and Machines, 21(2): 323–336. doi:10.1007/s11023-011-9231-5

• –––, 2017, “Explaining engineered computing systems’ behaviour: the role of abstraction and idealization”, Philosophy & Technology, 30(2): 239–258.

• Anscombe, G. E. M., 1963, Intention, second edition, Oxford: Blackwell.

• Arkoudas, Konstantine & Selmer Bringsjord, 2007, “Computers, Justification, and Mathematical Knowledge”, Minds and Machines, 17(2): 185–202. doi:10.1007/s11023-007-9063-5

• Arif, R. Mori, E., and Primiero, G, 2018, “Validity and Correctness before the OS: the case of LEOI and LEOII”, in Liesbeth de Mol, Giuseppe Primiero (eds.), Reflections on Programmings Systems - Historical and Philosophical Aspects, Philosophical Studies Series, Cham: Springer, pp. 15–47.

• Ashenhurst, Robert L. (ed.), 1989, “Letters in the ACM Forum”, Communications of the ACM, 32(3): 287. doi:10.1145/62065.315925

• Baier, A., 1970, “Act and Intent”, Journal of Philosophy, 67: 648–658.

• Baier, Christel & Joost-Pieter Katoen, 2008, Principles of Model Checking, Cambridge, MA: The MIT Press.

• Bass, Len, Paul C. Clements, & Rick Kazman, 2003 [1997], Software Architecture in Practice, second edition, Reading, MA: Addison-Wesley; first edition 1997; third edition, 2012.

• Bechtel, William & Adele Abrahamsen, 2005, “Explanation: A Mechanist Alternative”, Studies in History and Philosophy of Science Part C: Studies in History and Philosophy of Biological and Biomedical Sciences, 36(2): 421–441. doi:10.1016/j.shpsc.2005.03.010

• Boghossian, Paul A., 1989, “The Rule-following Considerations”, Mind, 98(392): 507–549. doi:10.1093/mind/XCVIII.392.507

• Bourbaki, Nicolas, 1968, Theory of Sets, Ettore Majorana International Science Series, Paris: Hermann.

• Bratman, M. E., 1987, Intention, Plans, and Practical Reason, Cambridge, MA: Harvard University Press.

• Bridges, Douglas & Palmgren Erik, 2013, “Constructive Mathematics”, The Stanford Encyclopedia of Philosophy (Winter 2013 Edition), Edward N. Zalta (ed.), URL = <Constructive Mathematics (Stanford Encyclopedia of Philosophy/Winter 2013 Edition)>.

• Brooks, Frederick P. Jr., 1995, The Mythical Man Month: Essays on Software Engineering, Anniversary Edition, Reading, MA: Addison-Wesley.

• –––, 1996, “The Computer Scientist as Toolsmith II”, Communications of the ACM, 39(3): 61–68. doi:10.1145/227234.227243

• Burge, Tyler, 1998, “Computer Proof, Apriori Knowledge, and Other Minds”, Noûs, 32(S12): 1–37. doi:10.1111/0029-4624.32.s12.1

• Bynum, Terrell Ward, 2008, “Milestones in the History of Information and Computer Ethics”, in Himma and Tavani 2008: 25–48. doi:10.1002/9780470281819.ch2

• Callahan, John, Francis Schneider, & Steve Easterbrook, 1996, “Automated Software Testing Using Model-Checking”, in Proceeding Spin Workshop, J.C. Gregoire, G.J. Holzmann and D. Peled (eds.), New Brunswick, NJ: Rutgers University, pp. 118–127.

• Cardelli, Luca & Peter Wegner, 1985, “On Understanding Types, Data Abstraction, and Polymorphism”, 17(4): 471–522. [Cardelli and Wegner 1985 available online]

• Carnap, R., 1966, Philosophical foundations of physics (Vol. 966), New York: Basic Books.

• Carrara, M., Gaio, S., and Soavi, M., 2014, “Artifact kinds, identity criteria, and logical adequacy”, in M. Franssen, P. Kroes, T. Reydon and P. E. Vermaas (eds.), Artefact Kinds: Ontology and The Human-made World, New York: Springer, pp. 85–101.

• Chalmers, A. F., 1999, What is this thing called Science?, Maidenhead: Open University Press

• Chalmers, David J., 1996, “Does a Rock Implement Every Finite-State Automaton?” Synthese, 108(3): 309–33. [D.J. Chalmers 1996 available online] doi:10.1007/BF00413692

• Clarke, Edmund M. Jr., Orna Grumberg, & Doron A. Peled, 1999, Model Checking, Cambridge, MA: The MIT Press.

• Colburn, Timothy R., 1999, “Software, Abstraction, and Ontology”, The Monist, 82(1): 3–19. doi:10.5840/monist19998215

• –––, 2000, Philosophy and Computer Science, Armonk, NY: M.E. Sharp.

• Colburn, T. R., Fetzer, J. H. , and Rankin T. L., 1993, Program Verification: Fundamental Issues in Computer Science, Dordrecht: Kluwer Academic Publishers.

• Colburn, Timothy & Gary Shute, 2007, “Abstraction in Computer Science”, Minds and Machines, 17(2): 169–184. doi:10.1007/s11023-007-9061-7

• Copeland, B. Jack, 1993, Artificial Intelligence: A Philosophical Introduction, San Francisco: John Wiley & Sons.

• –––, 1996, “What is Computation?” Synthese, 108(3): 335–359. doi:10.1007/BF00413693

• –––, 2015, “The Church-Turing Thesis”, The Stanford Encyclopedia of Philosophy (Summer 2015 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/sum2015/entries/church-turing/.

• Copeland, B. Jack & Oron Shagrir, 2007, “Physical Computation: How General are Gandy’s Principles for Mechanisms?” Minds and Machines, 17(2): 217–231. doi:10.1007/s11023-007-9058-2

• –––, 2011, “Do Accelerating Turing Machines Compute the Uncomputable?” Minds and Machines, 21(2): 221–239. doi:10.1007/s11023-011-9238-y

• Cummins, Robert, 1975, “Functional Analysis”, The Journal of Philosophy, 72(20): 741–765. doi:10.2307/2024640

• Davidson, D., 1963, “Actions, Reasons, and Causes,” reprinted in Essays on Actions and Events, Oxford: Oxford University Press, 1980, pp. 3–20.

• –––, 1978, “Intending”, reprinted in Essays on Actions and Events, Oxford: Oxford University Press, 1980, pp. 83–102.

• De Millo, Richard A., Richard J. Lipton, & Alan J. Perlis, 1979, “Social Processes and Proofs of Theorems and Programs”, Communications of the ACM, 22(5): 271–281. doi:10.1145/359104.359106

• Denning, Peter J., 2005, “Is Computer Science Science?”, Communications of the ACM, 48(4): 27–31. doi:10.1145/1053291.1053309

• –––, 2007, “Computing is a Natural Science”, Communications of the ACM, 50(7): 13–18. doi:10.1145/1272516.1272529

• Denning, Peter J., Edward A. Feigenbaum, Paul Gilmore, Anthony C. Hearn, Robert W. Ritchie, & Joseph F. Traub, 1981, “A Discipline in Crisis”, Communications of the ACM, 24(6): 370–374. doi:10.1145/358669.358682

• Devlin, Keith, 1994, Mathematics: The Science of Patterns: The Search for Order in Life, Mind, and the Universe, New York: Henry Holt.

• Dijkstra, Edsger W., 1970, Notes on Structured Programming, T.H.-Report 70-WSK-03, Mathematics Technological University Eindhoven, The Netherlands. [Dijkstra 1970 available online]

• –––, 1974, “Programming as a Discipline of Mathematical Nature”, American Mathematical Monthly, 81(6): 608–612. [Dijkstra 1974 available online

• Distributed Software Engineering, 1997, The Darwin Language, Department of Computing, Imperial College of Science, Technology and Medicine, London. [Darwin language 1997 available online]

• Duhem, P., 1954, The Aim and Structure of Physical Theory, Princeton: Princeton University Press.

• Duijf, H., Broersen, J., and Meyer, J. J. C., 2019, “Conflicting intentions: rectifying the consistency requirements”, Philosophical Studies, 176(4): 1097–1118.

• Dummett, Michael A.E., 2006, Thought and Reality, Oxford: Oxford University Press.

• Duncan, William, 2011, “Using Ontological Dependence to Distinguish between Hardware and Software”, Proceedings of the Society for the Study of Artificial Intelligence and Simulation of Behavior Conference: Computing and Philosophy, University of York, York, UK. [Duncan 2011 available online (zip file)]

• –––, 2017, “Ontological Distinctions between Hardware and Software”, Applied Ontology, 12(1): 5–32.

• Eden, Amnon H., 2007, “Three Paradigms of Computer Science”, Minds and Machines, 17(2): 135–167. doi:10.1007/s11023-007-9060-8

• Egan, Frances, 1992, “Individualism, Computation, and Perceptual Content”, Mind, 101(403): 443–59. doi:10.1093/mind/101.403.443

• Edgar, Stacey L., 2003 [1997], Morality and Machines: Perspectives on Computer Ethics, Sudbury, MA: Jones & Bartlett Learning.

• Ferrero, L., 2017, “Intending, Acting, and Doing,” Philosophical Explorations, 20 (Supplement 2): 13–39.

• Fernández, Maribel, 2004, Programming Languages and Operational Semantics: An Introduction, London: King’s College Publications.

• Fetzer, James H., 1988, “Program Verification: The Very Idea”, Communications of the ACM, 31(9): 1048–1063. doi:10.1145/48529.48530

• –––, 1990, Artificial Intelligence: Its Scope and Limits, Dordrecht: Springer Netherlands.

• Feynman, Richard P., 1984–1986, Feynman Lectures on Computation, Cambridge, MA: Westview Press, 2000.

• Flanagan, Mary, Daniel C. Howe, & Helen Nissenbaum, 2008, “Embodying Values in Technology: Theory and Practice”, in Information Technology and Moral Philosophy, Jeroen van den Hoven and John Weckert (eds.), Cambridge: Cambridge University Press, pp. 322–353.

• Floridi, Luciano, 2008, “The Method of Levels of Abstraction”, Minds and Machines, 18(3): 303–329. doi:10.1007/s11023-008-9113-7

• Floridi, Luciano, Nir Fresco, & Giuseppe Primiero, 2015, “On Malfunctioning Software”, Synthese, 192(4): 1199–1220. doi:10.1007/s11229-014-0610-3

• Floyd, Robert W., 1979, “The Paradigms of Programming”, Communications of the ACM, 22(8): 455–460. doi:10.1145/1283920.1283934

• Fowler, Martin, 2003, UML Distilled: A Brief Guide to the Standard Object Modeling Language, 3rd edition, Reading, MA: Addison-Wesley.

• Franssen, Maarten, Gert-Jan Lokhorst, & Ibio van de Poel, 2013, “Philosophy of Technology”, The Stanford Encyclopedia of Philosophy (Winter 2013 Edition), Edward N. Zalta (ed.), URL = <Philosophy of Technology (Stanford Encyclopedia of Philosophy/Winter 2013 Edition)>.

• Frege, Gottlob, 1914, “Letter to Jourdain”, reprinted in Frege 1980: 78–80.

• –––, 1980, Gottlob Frege: Philosophical and Mathematical Correspondence, G. Gabriel, H. Hermes, F. Kambartel, C. Thiel, and A. Veraart (eds.), Oxford: Blackwell Publishers.

• Fresco, Nir & Giuseppe Primiero, 2013, “Miscomputation”, Philosophy & Technology, 26(3): 253–272. doi:10.1007/s13347-013-0112-0

• Friedman, Batya & Helen Nissenbaum, 1996, “Bias in Computer Systems”, ACM Transactions on Information Systems (TOIS), 14(3): 330–347. doi:10.1145/230538.230561

• Frigg, Roman & Stephan Hartmann, 2012, “Models in Science”, The Stanford Encyclopedia of Philosophy (Fall 2012 Edition), Edward N. Zalta (ed.), URL =<Models in Science (Stanford Encyclopedia of Philosophy/Fall 2012 Edition)>.

• Gagliardi, Francesco, 2007, “Epistemological Justification of Test Driven Development in Agile Processes”, Agile Processes in Software Engineering and Extreme Programming: Proceedings of the 8th International Conference, XP 2007, Como, Italy, June 18–22, 2007, Berlin: Springer Berlin Heidelberg, pp. 253–256. doi:10.1007/978-3-540-73101-6_48

• Gamma, Erich, Richard Helm, Ralph Johnson, & John Vlissides, 1994, Design Patterns: Elements of Reusable Object-Oriented Software, Reading, MA: Addison-Wesley.

• Glennan, Stuart S., 1996, “Mechanisms and the Nature of Causation”, Erkenntnis, 44(1): 49–71. doi:10.1007/BF00172853

• Glüer, Kathrin & Åsa Wikforss, 2015, “The Normativity of Meaning and Content”, The Stanford Encyclopedia of Philosophy (Summer 2015 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/sum2015/entries/meaning-normativity/.

• Goguen, Joseph A. & Rod M. Burstall, 1985, “Institutions: Abstract Model Theory for Computer Science”, Report CSLI-85-30, Center for the Study of Language and Information at Stanford University.

• –––, 1992, “Institutions: Abstract Model Theory for Specification and Programming”, Journal of the ACM (JACM), 39(1): 95–146. doi:10.1145/147508.147524

• Gordon, Michael J.C., 1979, The Denotational Description of Programming Languages, New York: Springer-Verlag.

• Gotterbarn, Donald, 1991, “Computer Ethics: Responsibility Regained”, National Forum: The Phi Beta Kappa Journal, 71(3): 26–31.

• –––, 2001, “Informatics and Professional Responsibility”, Science and Engineering Ethics, 7(2): 221–230. doi:10.1007/s11948-001-0043-5

• Gotterbarn, Donald, Keith Miller, & Simon Rogerson, 1997, “Software Engineering Code of Ethics”, Information Society, 40(11): 110–118. doi:10.1145/265684.265699

• Gotterbarn, Donald & Keith W. Miller, 2009, “The Public is the Priority: Making Decisions Using the Software Engineering Code of Ethics”, IEEE Computer, 42(6): 66–73. doi:10.1109/MC.2009.204

• Gruner, Stefan, 2011, “Problems for a Philosophy of Software Engineering”, Minds and Machines, 21(2): 275–299. doi:10.1007/s11023-011-9234-2

• Gunter, Carl A., 1992, Semantics of Programming Languages: Structures and Techniques, Cambridge, MA: MIT Press.

• Gupta, Anil, 2014, “Definitions”, The Stanford Encyclopedia of Philosophy (Fall 2014 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/fall2014/entries/definitions/.

• Gurevich, Y., 2000, “Sequential Abstract-State Machines Capture Sequential Algorithms”, ACM Transactions on Computational Logic (TOCL), 1(1): 77-111.

• –––, 2012, “What is an algorithm?”, in International conference on current trends in theory and practice of computer science, Heidelberg, Berlin: Springer, pp. 31–42.

• Hacking, I., 2014, Why is there a Philosophy of Mathematics at all?, Cambridge: Cambridge University Press.

• Hagar, Amit, 2007, “Quantum Algorithms: Philosophical Lessons”, Minds and Machines, 17(2): 233–247. doi:10.1007/s11023-007-9057-3

• Hale, Bob, 1987, Abstract Objects, Oxford: Basil Blackwell.

• Hales, Thomas C., 2008, “Formal Proof”, Notices of the American Mathematical Society, 55(11): 1370–1380.

• Hankin, Chris, 2004, An Introduction to Lambda Calculi for Computer Scientists, London: King’s College Publications.

• Harrison, John, 2008, “Formal Proof—Theory and Practice”, Notices of the American Mathematical Society, 55(11): 1395–1406.

• Hartmanis, Juris, 1981, “Nature of Computer Science and Its Paradigms”, pp. 353–354 (in Section 1) of “Quo Vadimus: Computer Science in a Decade”, J.F. Traub (ed.), Communications of the ACM, 24(6): 351–369. doi:10.1145/358669.358677

• –––, 1993, “Some Observations About the Nature of Computer Science”, in International Conference on Foundations of Software Technology and Theoretical Computer Science, Springer Berlin Heidelberg, pp. 1–12. doi:10.1007/3-540-57529-4_39

• Hayes, P. J., 1997, “What is a Computer?”, The Monist, 80(3): 389–404.

• Hempel, C. G., 1970, “On the ‘standard conception’ of scientific theories”, Minnesota Studies in the Philosophy of Science, 4: 142–163.

• Henson, Martin C., 1987, Elements of Functional Programming, Oxford: Blackwell.

• Hilbert, David, 1931, “The Grounding of Elementary Number Theory”, reprinted in P. Mancosu (ed.), 1998, From Brouwer to Hilbert: the Debate on the Foundations of Mathematics in the 1920s, New York: Oxford University Press, pp. 266–273.

• Hilbert, David & Wilhelm Ackermann, 1928, Grundzüge Der Theoretischen Logik, translated as Principles of Mathematical Logic, Lewis M. Hammond, George G. Leckie, and F. Steinhardt (trans.), New York: Chelsea, 1950.

• Hill, R.K., 2016, “What an algorithm is”, Philosophy & Technology, 29(1): 35–59.

• –––, 2018, “Elegance in Software”, in Liesbeth de Mol, Giuseppe Primiero (eds.), Reflections on Programmings Systems - Historical and Philosophical Aspects (Philosophical Studies Series), Cham: Springer, pp. 273–286.

• Hoare, C.A.R., 1969, “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12(10): 576–580. doi:10.1145/363235.363259

• –––, 1973, “Notes on Data Structuring”, in O.J. Dahl, E.W. Dijkstra, and C.A.R. Hoare (eds.), Structured Programming, London: Academic Press, pp. 83–174.

• –––, 1981, “The Emperor’s Old Clothes”, Communications of the ACM, 24(2): 75–83. doi:10.1145/1283920.1283936

• –––, 1985, Communicating Sequential Processes, Englewood Cliffs, NJ: Prentice Hall. [Hoare 1985 available online]

• –––, 1986, The Mathematics of Programming: An Inaugural Lecture Delivered Before the University of Oxford on Oct. 17, 1985, Oxford: Oxford University Press.

• Hodges, Andrews, 2011, “Alan Turing”, The Stanford Encyclopedia of Philosophy (Summer 2011 Edition), Edward N. Zalta (ed.), URL = <Alan Turing (Stanford Encyclopedia of Philosophy/Summer 2011 Edition)>.

• Hodges, Wilfrid, 2013, “Model Theory”, The Stanford Encyclopedia of Philosophy (Fall 2013 Edition), Edward N. Zalta (ed.), forthcoming URL = <Model Theory (Stanford Encyclopedia of Philosophy/Fall 2013 Edition)>.

• Hopcroft, John E. & Jeffrey D. Ullman, 1969, Formal Languages and their Relation to Automata, Reading, MA: Addison-Wesley.

• Hughes, Justin, 1988, “The Philosophy of Intellectual Property”, Georgetown Law Journal, 77: 287.

• Irmak, Nurbay, 2012, “Software is an Abstract Artifact”, Grazer Philosophische Studien, 86(1): 55–72.

• Johnson, Christopher W., 2006, “What are Emergent Properties and How Do They Affect the Engineering of Complex Systems”, Reliability Engineering and System Safety, 91(12): 1475–1481. [Johnson 2006 available online]

• Johnson-Laird, P. N., 1988, The Computer and the Mind: An Introduction to Cognitive Science, Cambridge, MA: Harvard University Press.

• Jones, Cliff B., 1990 [1986], Systematic Software Development Using VDM, second edition, Englewood Cliffs, NJ: Prentice Hall. [Jones 1990 available online]

• Kimppa, Kai, 2005, “Intellectual Property Rights in Software—Justifiable from a Liberalist Position? Free Software Foundation’s Position in Comparison to John Locke’s Concept of Property”, in R.A. Spinello & H.T. Tavani (eds.), Intellectual Property Rights in a Networked World: Theory and Practice, Hershey, PA: Idea, pp. 67–82.

• Kinsella, N. Stephan, 2001, “Against Intellectual Property”, Journal of Libertarian Studies, 15(2): 1–53.

• Kleene, S. C., 1967, Mathematical Logic, New York: Wiley.

• Knuth, D. E., 1973, The Art of Computer Programming, second edition, Reading, MA: Addison-Wesley.

• –––, 1974a, “Computer Programming as an Art”, Communications of the ACM, 17(12): 667–673. doi:10.1145/1283920.1283929

• –––, 1974b, “Computer Science and Its Relation to Mathematics”, The American Mathematical Monthly, 81(4): 323–343.

• –––, 1977, “Algorithms”, Scientifc American, 236(4): 63–80.

• Kripke, Saul, 1982, Wittgenstein on Rules and Private Language, Cambridge, MA: Harvard University Press.

• Kroes, Peter, 2010, “Engineering and the Dual Nature of Technical Artefacts”, Cambridge Journal of Economics, 34(1): 51–62. doi:10.1093/cje/bep019

• –––, 2012, Technical Artefacts: Creations of Mind and Matter: A Philosophy of Engineering Design, Dordrecht: Springer.

• Kroes, Peter & Anthonie Meijers, 2006, “The Dual Nature of Technical Artefacts”, Studies in History and Philosophy of Science, 37(1): 1–4. doi:10.1016/j.shpsa.2005.12.001

• Kröger, Fred & Stephan Merz, 2008, Temporal Logics and State Systems, Berlin: Springer.

• Ladd, John, 1988, “Computers and Moral Responsibility: a Framework for An Ethical Analysis”, in Carol C. Gould, (ed.), The Information Web: Ethical & Social Implications of Computer Networking, Boulder, CO: Westview Press, pp. 207–228.

• Landin, P.J., 1964, “The Mechanical Evaluation of Expressions”, The Computer Journal, 6(4): 308–320. doi:10.1093/comjnl/6.4.308

• Littlewood, Bev & Lorenzo Strigini, 2000, “Software Reliability and Dependability: a Roadmap”, ICSE ’00 Proceedings of the Conference on the Future of Software Engineering, pp. 175–188. doi:10.1145/336512.336551

• Locke, John, 1690, The Second Treatise of Government. [Locke 1690 available online]

• Loewenheim, Ulrich, 1989, “Legal Protection for Computer Programs in West Germany”, Berkeley Technology Law Journal, 4(2): 187–215. [Loewenheim 1989 available online] doi:10.15779/Z38Q67F

• Long, Roderick T., 1995, “The Libertarian Case Against Intellectual Property Rights”, Formulations, Autumn, Free Nation Foundation.

• Loui, Michael C. & Keith W. Miller, 2008, “Ethics and Professional Responsibility in Computing”, Wiley Encyclopedia of Computer Science and Engineering, Benjamin Wah (ed.), John Wiley & Sons. [Loui and Miller 2008 available online]

• Lowe, E. J., 1998, The Possibility of Metaphysics: Substance, Identity, and Time, Oxford: Clarendon Press.

• Luckham, David C., 1998, “Rapide: A Language and Toolset for Causal Event Modeling of Distributed System Architectures”, in Y. Masunaga, T. Katayama, and M. Tsukamoto (eds.), Worldwide Computing and its Applications, WWCA’98, Berlin: Springer, pp. 88–96. doi:10.1007/3-540-64216-1_42

• Machamer, Peter K., Lindley Darden, & Carl F. Craver, 2000, “Thinking About Mechanisms”, Philosophy of Science, 67(1): 1–25. doi:10.1086/392759

• Magee, Jeff, Naranker Dulay, Susan Eisenbach, & Jeff Kramer, 1995, “Specifying Distributed Software Architectures”, Proceedings of 5th European Software Engineering Conference (ESEC 95), Berlin: Springer-Verlag, pp. 137–153.

• Markov, A., 1954, “Theory of algorithms”, Tr. Mat. Inst. Steklov 42, pp. 1–14. trans. by Edwin Hewitt in American Mathematical Society Translations, Series 2, Vol. 15 (1960).

• Martin-Löf, Per, 1982, “Constructive Mathematics and Computer Programming”, in Logic, Methodology and Philosophy of Science (Volume VI: 1979), Amsterdam: North-Holland, pp. 153–175.

• McGettrick, Andrew, 1980, The Definition of Programming Languages, Cambridge: Cambridge University Press.

• McLaughlin, Peter, 2001, What Functions Explain: Functional Explanation and Self-Reproducing Systems, Cambridge: Cambridge University Press.

• Meijers, A.W.M., 2001, “The Relational Ontology of Technical Artifacts”, in P.A. Kroes and A.W.M. Meijers (eds.), The Empirical Turn in the Philosophy of Technology, Amsterdam: Elsevier, pp. 81–96.

• Mitchelmore, Michael & Paul White, 2004, “Abstraction in Mathematics and Mathematics Learning”, in M.J. Høines and A.B. Fuglestad (eds.), Proceedings of the 28th Conference of the International Group for the Psychology of Mathematics Education (Volume 3), Bergen: Programm Committee, pp. 329–336. [Mitchelmore and White 2004 available online]

• Miller, Alexander & Crispin Wright (eds), 2002, Rule Following and Meaning, Montreal/Ithaca: McGill-Queen's University Press.

• Milne, Robert & Christopher Strachey, 1976, A Theory of Programming Language Semantics, London: Chapman and Hall.

• Milner, R., 1971, “An algebraic definition of simulation between programs”, Technical Report, CS-205, pp. 481–489, Department of Computer Science, Stanford University.

• Mitchell, John C., 2003, Concepts in Programming Languages, Cambridge: Cambridge University Press.

• Monin, Jean François, 2003, Understanding Formal Methods, Michael G. Hinchey (ed.), London: Springer (this is Monin's translation of his own Introduction aux Méthodes Formelles, Hermes, 1996, first edition; 2000, second edition), doi:10.1007/978-1-4471-0043-0

• Mooers, Calvin N., 1975, “Computer Software and Copyright”, ACM Computing Surveys, 7(1): 45–72. doi:10.1145/356643.356647

• Moor, James H., 1978, “Three Myths of Computer Science”, The British Journal for the Philosophy of Science, 29(3): 213–222.

• Morgan, C., 1994, Programming From Specifications, Englewood Cliffs: Prentice Hall. [Morgan 1994 available online]

• Moschovakis, Y. N., 2001, “What is an algorithm?”, in Mathematics Unlimited—2001 and Beyond, Heidelberg, Berlin: Springer, pp. 919–936.

• Naur, P., 1985, “Programming as theory building”, Microprocessing and microprogramming, 15(5): 253–261.

• Newell, A., and Simon, H. A., 1961, “Computer simulation of human thinking” Science, 134(3495): 2011–2017.

• ––– 1972, Human Problem Solving, Englewood Cliffs, NJ: Prentice-Hall.

• –––, 1976, “Computer Science as Empirical Inquiry: Symbols and Search”, Communications of the ACM, 19(3): 113–126. doi:10.1145/1283920.1283930

• Newell, Allen, Alan J. Perlis, & Herbert A. Simon, 1967, “Computer Science”, Science, 157(3795): 1373–1374. doi:10.1126/science.157.3795.1373-b

• Nissenbaum,Helen, 1998, “Values in the Design of Computer Systems”, Computers and Society, 28(1): 38–39.

• Northover, Mandy, Derrick G. Kourie, Andrew Boake, Stefan Gruner, & Alan Northover, 2008, “Towards a Philosophy of Software Development: 40 Years After the Birth of Software Engineering”, Journal for General Philosophy of Science, 39(1): 85–113. doi:10.1007/s10838-008-9068-7

• Pears, David Francis, 2006, Paradox and Platitude in Wittgenstein’s Philosophy, Oxford: Oxford University Press. doi:10.1093/acprof:oso/9780199247707.001.0001

• Piccinini, Gualtiero, 2007, “Computing Mechanisms”, Philosophy of Science, 74(4): 501–526. doi:10.1086/522851

• –––, 2008, “Computation without Representation”, Philosophical Studies, 137(2): 206–241. [Piccinini 2008 available online] doi:10.1007/s11098-005-5385-4

• –––, 2008, “Computers”, Pacific Philosophical Quarterly, 89: 32–73.

• –––, 2015, Physical Computation: A Mechanistic Account, Oxford: Oxford University Press. doi:10.1093/acprof:oso/9780199658855.001.0001

• Piccinini, Gualtiero & Carl Craver, 2011, “Integrating Psychology and Neuroscience: Functional Analyses as Mechanism Sketches”, Synthese, 183(3): 283–311. doi:10.1007/s11229-011-9898-4

• Popper, Karl R., 1959, The Logic of Scientific Discovery, London: Hutchinson.

• Primiero, G., 2016, “Information in the philosophy of computer science”, in Floridi L. (ed.), The Routledge Handbook of Philosophy of Information, London: Routledge, pp. 90–106.

• –––, 2020, On the Foundations of Computing. New York: Oxford University Press.

• Primiero, G., D.F. Solheim & J.M. Spring, 2019 “On Malfunction, Mechanisms and Malware Classification”, Philos. Technol. 32: 339–362. https://doi.org/10.1007/s13347-018-0334-2

• Pylyshyn, Z. W., 1984, Computation and Cognition: Towards a Foundation for Cognitive Science, Cambridge, MA: MIT Press.

• Pym, D., J.M. Spring, & P. O’Hearn, 2019, “Why Separation Logic Works”, Philosophy & Technology, 32: 483–516.

• Rapaport, William J., 1995, “Understanding Understanding: Syntactic Semantics and Computational Cognition”, in Tomberlin (ed.), Philosophical Perspectives, Vol. 9: AI, Connectionism, and Philosophical Psychology, Atascadero, CA: Ridgeview, pp. 49–88. [Rapaport 1995 available online] doi:10.2307/2214212

• –––, 1999, “Implementation Is Semantic Interpretation”, The Monist, 82(1): 109–30. [Rapaport 1999 available online]

• –––, 2005, “Implementation as Semantic Interpretation: Further Thoughts”, Journal of Experimental& Theoretical Artificial Intelligence, 17(4): 385–417. [Rapaport 2005 available online]

• –––, 2012, “Semiotic systems, computers, and the mind: how cognition could be computing”, International Journal of Signs and Semiotic Systems, 2(1): 32–71

• –––, 2018, “What is a Computer? A Survey”, Minds and Machines, 28(3): 385–426.

• Reynolds, J.C., 2002, “Separation Logic: a logic for shared mutable data structures”, in Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, IEEE, pp. 55–74.

• Rombach, Dieter & Frank Seelisch, 2008, “Formalisms in Software Engineering: Myths Versus Empirical Facts”, in Balancing Agility and Formalism in Software Engineering, Springer Berlin Heidelberg, pp. 13–25. doi:10.1007/978-3-540-85279-7_2

• Rosenberg, A., 2012, The Philosophy of Science, London: Routledge.

• Ryle G., 1949 [2009], The Concept of Mind, Abingdon: Routledge

• Schiaffonati, Viola, 2015, “Stretching the Traditional Notion of Experiment in Computing: Explorative Experiments”, Science and Engineering Ethics, 22(3): 1–19. doi:10.1007/s11948-015-9655-z

• Schiaffonati, Viola & Mario Verdicchio, 2014, “Computing and Experiments”, Philosophy & Technology, 27(3): 359–376. doi:10.1007/s13347-013-0126-7

• Searle, J. R., 1990, “Is the brain a digital computer?” Proceedings and Addresses of the American Philosophical Association, 64(3): 21–37.

• Searle, John R., 1995, The Construction of Social Reality, New York: Free Press.

• Setiya, K., “Intention”, The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/fall2018/entries/intention/.

• Shanker, S.G., 1987, “Wittgenstein versus Turing on the Nature of Church’s Thesis”, Notre Dame Journal of Formal Logic, 28(4): 615–649. [Shanker 1987 available online] doi:10.1305/ndjfl/1093637650

• Shavell, Steven & Tanguy van Ypersele, 2001, “Rewards Versus Intellectual Property Rights”, Journal of Law and Economics, 44: 525–547

• Skemp, Richard R., 1987, The Psychology of Learning Mathematics, Hillsdale, NJ: Lawrence Erlbaum Associates.

• Smith, Brian Cantwell, 1985, “The Limits of Correctness in Computers”, ACM SIGCAS Computers and Society, 14–15(1–4): 18–26. doi:10.1145/379486.379512

• Snelting, Gregor, 1998, “Paul Feyerabend and Software Technology”, Software Tools for Technology Transfer, 2(1): 1–5. doi:10.1007/s100090050013

• Sommerville, Ian, 2016 [1982], Software Engineering, Reading, MA: Addison-Wesley; first edition, 1982.

• Sprevak, M., 2010, “Computation, individuation, and the received view on representation”, Studies in History and Philosophy of Science, 41(3): 260–270.

• –––, 2012, “Three Challenges to Chalmers on Computational Implementation”, Journal of Cognitive Science, 13(2): 107–143.

• Stoy, Joseph E., 1977, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics, Cambridge, MA: MIT Press.

• Strachey, Christopher, 2000, “Fundamental Concepts in Programming Languages”, Higher-Order and Symbolic Computation, 13(1–2): 11–49. doi:10.1023/A:1010000313106

• Suber, Peter, 1988, “What Is Software?” Journal of Speculative Philosophy, 2(2): 89–119. [Suber 1988 available online]

• Summerville, I., 2012, Software Engineering, Reading, MA: Addison-Wesley; first edition, 1982.

• Suppe, Frederick, 1989, The Semantic Conception of Theories and Scientific Realism, Chicago: University of Illinois Press.

• Suppes, Patrick, 1960, “A Comparison of the Meaning and Uses of Models in Mathematics and the Empirical Sciences”, Synthese, 12(2): 287–301. doi:10.1007/BF00485107

• –––, 1969, “Models of Data”, in Studies in the Methodology and Foundations of Science, Dordrecht: Springer Netherlands, pp. 24–35.

• Technical Correspondence, Corporate, 1989, Communications of the ACM, 32(3): 374–381. Letters from James C. Pleasant, Lawrence Paulson/Avra Cohen/Michael Gordon, William Bevier/Michael Smith/William Young, Thomas Clune, Stephen Savitzky, James Fetzer. doi:10.1145/62065.315927

• Tedre, Matti, 2011, “Computing as a Science: A Survey of Competing Viewpoints”, Minds and Machines, 21(3): 361–387. doi:10.1007/s11023-011-9240-4

• –––, 2015, The Science of Computing: Shaping a Discipline, Boca Raton: CRC Press, Taylor and Francis Group.

• Tedre, Matti & Ekki Sutinen, 2008, “Three Traditions of Computing: What Educators Should Know”, Computer Science Education, 18(3): 153–170. doi:10.1080/08993400802332332

• Thagard, P., 1984, “Computer programs as psychological theories”, Mind, Language and Society, Vienna: Conceptus-Studien, pp. 77–84.

• Thomasson, Amie, 2007, “Artifacts and Human Concepts”, in Eric Margolis and Stephen Laurence (eds.), Creations of the Mind: Essays on Artifacts and Their Representations, Oxford: Oxford University Press, pp. 52–73.

• Thompson, Simon, 2011, Haskell: The Craft of Functional Programming, third edition, Reading, MA: Addison-Wesley; first edition, 1996.

• Tichy, Walter F., 1998, “Should Computer Scientists Experiment More?”, IEEE Computer, 31(5): 32–40. doi:10.1109/2.675631

• Turing, A.M., 1936, “On Computable Numbers, with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society (Series 2), 42: 230–65. doi:10.1112/plms/s2-42.1.230

• –––, 1950, “Computing Machinery and Intelligence”, Mind, 59(236): 433–460. doi:10.1093/mind/LIX.236.433

• Turner, Raymond, 2007, “Understanding Programming Languages”, Minds and Machines, 17(2): 203–216. doi:10.1007/s11023-007-9062-6

• –––, 2009a, Computable Models, Berlin: Springer. doi:10.1007/978-1-84882-052-4

• –––, 2009b, “The Meaning of Programming Languages”, APA Newsletters, 9(1): 2–7. (This APA Newsletter is available online; see the Other Internet Resources.)

• –––, 2010, “Programming Languages as Mathematical Theories”, in J. Vallverdú (ed.), Thinking Machines and the Philosophy of Computer Science: Concepts and Principles, Hershey, PA: IGI Global, pp. 66–82.

• –––, 2011, “Specification”, Minds and Machines, 21(2): 135–152. doi:10.1007/s11023-011-9239-x

• –––, 2012, “Machines”, in H. Zenil (ed.), A Computable Universe: Understanding and Exploring Nature as Computation, London: World Scientific Publishing Company/Imperial College Press, pp. 63–76.

• –––, 2014, “Programming Languages as Technical Artefacts”, Philosophy and Technology, 27(3): 377–397; first published online 2013. doi:10.1007/s13347–012–0098-z

• –––, 2018, Computational artifacts: Towards a philosophy of computer science, Berlin Heidelberg: Springer.

• Tymoczko, Thomas, 1979, “The Four Color Problem and Its Philosophical Significance”, The Journal of Philosophy, 76(2): 57–83. doi:10.2307/2025976

• –––, 1980, “Computers, Proofs and Mathematicians: A Philosophical Investigation of the Four-Color Proof”, Mathematics Magazine, 53(3): 131–138.

• Van Fraassen, Bas C., 1980, The Scientific Image, Oxford: Oxford University Press. doi:10.1093/0198244274.001.0001

• –––, 1989, Laws and Symmetry, Oxford: Oxford University Press. doi:10.1093/0198248601.001.0001

• Van Leeuwen, Jan (ed.), 1990, Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics, Amsterdam: Elsevier and Cambridge, MA: MIT Press.

• Vardi, M., 2012, “What is an algorithm?”, Communications of the ACM, 55(3): 5. doi:10.1145/2093548.2093549

• Vermaas, Pieter E. & Wybo Houkes, 2003, “Ascribing Functions to Technical Artifacts: A Challenge to Etiological Accounts of Function”, British Journal of the Philosophy of Science, 54: 261–289. [Vermaas and Houkes 2003 available online]

• Vliet, Hans van, 2008, Software Engineering: Principles and Practice, 3rd edition, Hoboken, NJ: Wiley. (First edition, 1993)

• von Neumann, J. (1945). “First draft report on the EDVAC”, IEEE Annals of the History of Computing, 15(4): 27–75.

• Wang, Hao, 1974, From Mathematics to Philosophy, London: Routledge, Kegan & Paul.

• Wegner, Peter, 1976, “Research Paradigms in Computer Science”, in Proceedings of the 2nd international Conference on Software Engineering, Los Alamitos, CA: IEEE Computer Society Press, pp. 322–330.

• White, Graham, 2003, “The Philosophy of Computer Languages”, in Luciano Floridi (ed.), The Blackwell Guide to the Philosophy of Computing and Information, Malden: Wiley-Blackwell, pp. 318–326. doi:10.1111/b.9780631229193.2003.00020.x

• Wiener, Norbert, 1948, Cybernetics: Control and Communication in the Animal and the Machine, New York: Wiley & Sons.

• –––, 1964, God and Golem, Inc.: A Comment on Certain Points Where Cybernetics Impinges on Religion, Cambridge, MA: MIT press.

• Wittgenstein, Ludwig, 1953 [2001], Philosophical Investigations, translated by G.E.M. Anscombe, 3rd Edition, Oxford: Blackwell Publishing.

• –––, 1956 [1978], Remarks of the Foundations of Mathematics, G.H. von Wright, R. Rhees, and G.E.M. Anscombe (eds.), translated by G.E.M. Anscombe, revised edition, Oxford: Basil Blackwell.

• –––, 1939 [1975], Wittgenstein’s Lectures on the Foundations of Mathematics, Cambridge 1939, C. Diamond (ed.), Cambridge: Cambridge University Press.

• Woodcock, Jim & Jim Davies, 1996, Using Z: Specification, Refinement, and Proof, Englewood Cliffs, NJ: Prentice Hall.

• Wright, Crispin 1983, Frege’s Conception of Numbers as Objects, Aberdeen: Aberdeen University Press.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at the Friends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entry at PhilPapers, with links to its database.

Other Internet Resources

• ACM (ed.), 2013, ACM Turing Award Lectures.

• APA Newsletter on Philosophy and Computers, 9(1): Fall 2009.

• Groklaw, 2012a, “What Does ‘Software is Mathematics’ Mean?” Part 1, by PoIR.

• Groklaw, 2012b, “What Does ‘Software is Mathematics’ Mean?” Part 2, by PoIR.

• Huss, Eric, 1997, The C Library Reference Guide, at Fortran 90+ (www.fortran-2000.com).

• Rapaport, William J., 2020, “Philosophy of Computer Science”. DRAFT © 2004–2020 by William J. Rapaport. Available at Philosophy of Computer Science, manuscript.

• Smith, Barry, 2012, “Logic and Formal Ontology”. A revised version of the paper which appeared in J. N. Mohanty and W. McKenna (eds), 1989, Husserl’s Phenomenology: A Textbook, Lanham: University Press of America.

• Turner, Ray and Amon Eden, 2011, “The Philosophy of Computer Science”, Stanford Encyclopedia of Philosophy (Winter 2011 Edition), Edward N. Zalta (ed.), URL = <The Philosophy of Computer Science (Stanford Encyclopedia of Philosophy/Winter 2011 Edition)>. [This was the previous entry on the philosophy of computer science in the Stanford Encyclopedia of Philosophy—see the version history.]

Related Entries

artificial intelligence: logic-based | Church-Turing Thesis | computability and complexity | computation: in physical systems | computational complexity theory | information | information: semantic conceptions of | intention | mathematics, philosophy of | recursive functions | technology, philosophy of | Turing machines

Copyright © 2021 by Nicola Angius <[e-mail]> Giuseppe Primiero <[e-mail]> Raymond Turner <[e-mail]>