计算机科学哲学（四）
6.2 测试和实验
测试是启动程序并观察其执行以评估其是否符合所提供的属性规范的更“经验”的过程。这种技术在软件开发过程中得到广泛使用。哲学家和具有哲学思想的计算机科学家在科学发现的传统方法论方法的指导下考虑了软件测试（Snelting 1998；Gagliardi 2007；Northover 等 2008；Angius 2014），并质疑软件测试是否可以被视为评估程序正确性的科学实验（Schiaffonati 和 Verdicchio 2014，Schiaffonati 2015；Tedre 2015）。
Dijkstra 的著名格言“程序测试可用于显示错误的存在，但绝不能显示错误的不存在”（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% 正确），软件测试被认为是成功的。接下来的步骤是找出导致执行不正确的原因，即追溯错误（更熟悉的名称是“错误”），然后进入调试阶段，然后再次测试系统。换句话说，要对观察到的错误计算提出解释。
人们已经努力考虑计算机科学中的解释（Piccinini 2007；Piccinini 和 Craver 2011；Piccinini 2015；Angius 和 Tamburrini 2016）与科学哲学中阐述的不同解释模型的关系。具体而言，计算解释可以理解为一种特定类型的机械解释（Glennan 1996；Machamer 等 2000；Bechtel 和 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 数学正确性
形式化验证方法允许对程序的行为进行先验分析，而无需观察程序的任何实现或考虑其执行。特别是，定理证明允许人们从合适的公理表示中推断出所考虑程序的任何潜在行为及其行为属性。在模型检查的情况下，人们通过对给定集合论模型中有效的公式进行算法搜索，提前知道程序执行所显示的行为属性。这些考虑因素使 Hoare（1969 年）得出了著名的结论：程序开发是一门“精确科学”，其特征应该是正确性的数学证明，在认识论上与数学实践中的标准证明相当。
De Millo等。 （1979年）问题HOARE的论文：正确的数学证据通常是优雅和可掌握的，这意味着任何（专家）读者都可以“看到”所在地所遵循的结论（对于软件中优雅的概念，也可以看到Hill（2018））。 通常称为笛卡尔证明（黑客2014）在正确的证据中没有对应物，通常是长而繁琐的，难以掌握，而不是解释所以结论必然来自房屋的原因。 然而，由于使用lemmas，抽象和新概念的分析逐步逐步证明，它们主要是可调查的数学证明，但它们主要是可调查的。 相反，不涉及创建新概念的正确性证明，也不涉及一个通常在数学证据中找到的模块化（Turner，2018）。 然而，不可调查的证据不能被视为数学证明（Wittgenstein 1956）。
关于计算机程序的正确证据的第二种理论困难涉及它们的复杂性和待验证的程序的复杂性。 已经HOARE（1981）承认，虽然原则上始终可能验证正确性，但实际上它几乎无法实现。 除了琐碎的情况外，当代软件是模块化的编码，需要满足大量规格，它是开发的，以便与其他程序，系统，用户互动。 嵌入式和无功软件是点的情况。 为了验证这些复杂的软件，将自动执行正确性证明。 因此，一方面，正确的问题从检查的程序转移到执行验证的程序，例如， 定理箴言; 另一方面，由于机器的机械错误，物理过程进行的证明可能会出错。 针对这个无限的回归论证，Arkoudas和Bringsjord（2007）争辩说，一个可以使用一个证据检查员，通过是一个相对较小的程序，通常更易于验证。
最近，基于逻辑和统计分析的组合来检查正确性的正式方法对该研究领域的新刺激提供了新的刺激：分离逻辑（Reynolds，2002）的能力，提供计算系统物理内存的逻辑行为的表示，以及可能性考虑到输入的概率分布作为统计错误的统计来源，允许正式的正确检查大型交互式系统，如Facebook平台（另请参阅Pym等人。2019）。
7.2物理正确性
Fetzer（1988）反对，Defuctive推理只能能够保证方案关于其规范的正确性，而不是用于计算系统的正确性，这也占该程序的物理实现。 即使该程序对于任何相关的上限LOA（算法，规格，要求）是正确的，它的实现仍然可能由于物理发生故障而违反了一个或多个预期规范。 原则上的前一种正确性可以在数学上证明，但执行LOA的正确性需要经验评估。 如§6.2所检查，软件测试只能原则上显示计算系统的正确性。 在实践中，允许的非平凡系统的执行的数量是可能的无限的，并且不能以有限（或合理）的时间（Dijkstra 1974）详尽检查。 最成功的测试方法相反，相反，相同地看到与一起使用的正式验证和测试达到令人满意的校正级别。
另一个反对数学正确性的理论可能性的反对意见是，由于定理证明书，即物理机器，关于计算系统的知识，一个关于计算系统的知识不是先验的（参见特纳2018 CH.25）。 然而，Burge（1988）认为，基于计算机的正确性证明仍然可以被视为先验，因为即使他们的可能性取决于感官体验，他们的理由不是（因为它是用于A-Bouthiori知识）。 例如，即使它需要具有红色的感觉体验，红色是颜色的知识也是一个先验的 这是因为“红色是一种颜色”是真实的，独立于任何感官体验。 进一步讨论计算机在数学证明中使用计算机的性质，参见（Hales 2008;哈里森2008; Tymoczko 1979,1980）。
正确性的问题最终减少了询问物理机器的意味着满足抽象要求。 根据简单的映射帐户，计算系统S仅在以下情况下是正确的规范SP实现
可以从归因于SP所定义的州的州和SP所定义的国家建立态势
对于任何国家过渡
s
1
→
s
2
�
1
→
�
2
在s中有一个国家过渡
s
'
1
→
s
'
2
�
1
'
→
�
2
'
在国家之间
s
'
1
�
1
'
映射到
s
1
�
1
和州
s
'
2
�
2
'
映射到
s
2
�
2
。
简单的映射帐户仅需要在S和SP的描述之间进行扩展协议。 本述评的弱点是，在任何几个物理系统 - 规范之间识别延伸协议，留下了一个留下的小组诉讼者的观点（安德森和Piccinini 2024）。
Pancomputationations的危险导致了一些作者来尝试考虑正确的实施，以至于某种方式限制可能的解释类别。 特别是
因果账户（D. J. Chalmers 1996; Copeland 1996）表明材料有条件（如果系统处于物理状态
s
1
�
1
......）被反事实地替换。
语义账户认为计算系统必须与语义描述相关联，指定系统是实现的（Sprevak 2012）。 例如，物理设备可以被解释为AND门或A或门，但是没有设备的定义，没有办法定影伪像是什么。
语法账户需要只能定义为句法的物理状态可以映射到计算状态。 还有待检查的是定义句法状态的原因（请参阅Piccinini 2015或物理系统中的计算，以概述句法账户）。
规范性账户（Turner 2012）不仅维持摘要和物理计算过程必须在协议中，而且还具有在系统上具有规范力的规范力。 根据这样的帐户，计算是通过抽象规范来固定的物理过程。 这种关系比语义账户更强大，询问简单的描述关系和句法账户，专注于句法对象及其语义解释。
强大的帐户（Anderson和Piccinini 2024）认为，在其符合稳健的计算描述的情况下，系统是计算的，即当物理状态和计算状态之间的映射稳定可靠时。 当物理状态映射到承载相同的计算信息的计算状态时，映射在对物理系统的小扰动前方的弹性稳定时稳定。
7.3失误
到目前为止所说的情况，所实施的程序的正确性不会自动建立计算系统的良好运行。 图灵（1950）已经区分了功能的错误和结论错误。 前者是由无法执行某些高级语言程序的指令的错误实现引起的; 结论的错误表征了正确的抽象机器，尽管如此，仍未执行他们应该完成的任务。 这可能会发生在这些情况下，其中程序实例化正确的某些规格，该规格不会正确表达对此类程序的要求。 在这两种情况下，仍然可以说实施正确程序的机器误解。
图灵的功能与结论的错误误差的区别已扩展到一个完整的误传分类（Fresco和Primiero 2013）。 分类是基于定义计算系统的不同LOA来建立的。 错误可以是：
概念：它们违反了需要在命题联合正常形式表达的规范的一致性的有效条件;
材料：它们违反了计划关于其规范的正确性要求;
可执行的：当某些故障实现硬件突破物理限制时，它们会出现。
可执行的错误仅在执行级别下清楚地出现，并且它们对应于图灵的（1950）运行错误，也称为操作故障。 概念和物质错误可能会在任何级别从意图水平降至物理实施级别的抽象级别。 概念错误会出错，而材料错误会导致失败。 例如，意图级别的错误包括一个不一致的要求集，而在物理实现级别，它可以对应于无效的硬件设计（例如在逻辑门的选择中的真实功能连接的逻辑门）。 在规范级别发生的故障可能是由于设计对所需功能要求的集合不完整的设计，而算法级别的故障发生在那些常见的情况下，其中不符合规范。 超越错误，失败和运营故障，SLIPS是高级编程语言指令的误传级别：由于分别是分别，句法或语义缺陷，它们可能是概念性或物质错误。 概念滑动出现在所有这些案例中，其中侵犯了高级语言的语法规则; 材料滑动涉及违反编程语言的语义规则，例如当使用变量但未初始化时。
必须在基于软件的计算系统（Floridi，Fresco和Primiero 2015）之间的功能障碍和失控之间进行进一步的区分。 软件只能误会但不能进行功能障碍。 如果其物理实现无法满足意图或规格，软件令牌可以进行功能障碍。 功能障碍仅适用于单个代币，因为它的表达功能函数不像相同类型的其他代币相对于实现的功能。 因此，功能障碍不适用于意图水平和规范级别。 相反，软件类型和令牌都可以误障，因为断误不依赖于与能够执行一些实现的功能的同一类型的令牌的比较。 令牌的误操作通常取决于其他一些组件的功能障碍，而类型的误操作往往是由于设计不佳。 软件令牌无法进行功能障碍，因为给定类型的所有令牌实现统一指定的函数，以意图和规范级别统一。 这些功能在算法实现级别实现，然后在执行级别执行之前; 在实现正确的情况下，所有令牌都会在执行级别执行正确（如果没有发生操作故障）。
