英文链接在

     本文认为不断扩大的“计算机科学”使得传统科学与工程模式的研究难以维继。特别是在形式方法的研究上，目前的工作已经丢弃了传统经验方法。在需求工程和人机交互领域，形式方法的支持者们同样也面临着挑战。计算科学的用词不当是这些问题的起源。目前计算学科讨论的主题是技术而不是理论。这样，当学院以科学准则进行博士评估时就会产生问题。于是人们在开始更高学位的学习前，不禁要问自己“计算科学的研究到底是什么？”
这篇文章是为上高级硕士课程的学生或研究生新生作一个高水平的介绍。读者应结合阅读。
     关键词：research skills（研究技巧 ）, computing science（计算科学）.

1.引言

     成功的研究从好的定义开始。牛津简明词典是这样定义“研究”的：

reaserch. 1.

a the systematic investigation into and study of materials, sources, etc, in order to establish facts and reach new conclusions.

b. an endeavour to discover new or collate old facts etc by the scientific study of a subject or by a course of critical investigation.

     这一有用的定义侧重于研究的系统性。换句话说，这词的含义暗含了研究的方法。这些方法和系统本质上提供了逻辑论证的模型和结构。

1.1 研究的辩证关系

     在某一领域的框架之争里可以看到逻辑论证的最高形式。争论可以归结于以下三类：
论点：论文是想法的原始陈述。然而只有极少数研究成果可以说是完全独创的。大多数研究都要站在巨人的肩膀上，甚至是其它学科的巨人。
反对：这是对前人的研究提出质疑。通常，这种建立在新的事实证据上的论证是一个领域的进展。
综合：从已有的材料找寻新的观点。综合性的论点通常会解决一种论点及其对立面的明显矛盾。
     就比如说关于原型设计的争论。例如，一些学者认为在开发阶段初期，原型是生成和评价新设计的好方法（论点）（Fuchs，1992）。其它学者则提供证据反对这种假设。他们认为用户选择原型环境的特点时通常不考虑可能的替代方案（反对）（Hayes and Jones,1989）。接着，第三组研究者们开发出了一种技术以降低对原型环境的偏见（综合）（Gravell and Henderson,1996）。一个领域内的研究进展就是以这种方式，通过方法的实际应用去证明、反驳和重新评估论点。

2.模型论战

     更详细的逻辑论证可以在论述结构中找到。论述的结构可以用以支持个人工作的论点、反对或者综合。

2.1眼见为实

     也许制作一个可以代表通用解决方案的示例可以研究模型最直观，也最具有说服力。在计算机科学领域里，这种方法已经在很多场景下应用了。然而毫无疑问的是，多用户操作系统的实现难题更多地是通过UNIX的实现和发展而攻克的，而不是侧重测量的科学探究过程。
但是因为很多原因，这种方法对于研究来说并不是一个令人满意的模型。一个主要的原因就在于使用它的风险太大了。例如，所制作的示例很可能在我们得到任何有价值的信息之前就失败了。事实上，这种方法通常忽视了任何明显的假设和结论的形成直到示例制作完成。这会导致示例对于研究者越来越重要，而不是研究者们意图去建立的观点。
     一个清晰的假设不应该成为研究的阻碍。示例方法的证明手段在很多方面与工程实践是相同的。迭代精化可以使得一个实现逐步演变为一些理想的解决方案。过去失败的尝试能让研究人员更好定义研究进程中的目标。迭代开发的关键问题在于示例本身的开发也需要一种方法或结构。工程人员需要为认真仔细地规划开发计划，使得一次迭代中出现的错误可以在其下次迭代中得到反馈。通常，这可以通过基于科学论证的其它模型的测试技术完成。如此看来，工程学和科学技术本就存在着紧密的联系。
      engineering n. an application of science to the design, building and use of machines, construction etc. (牛津简明词典).

2.2经验主义

      我们可以将西方经验传统看作是在逃避无法直接解释的人工制品。它从17世纪起就建立最有统治力的研究。它可以归结为以下几个阶段：
        假设迭代：这一阶段确定需要通过研究测试的假设。
        方法确认：这一阶段确定用以证实假设的技术。这很重要，因为你的同行必须能审阅和评价你所选择的方法。雄厚的实证研究必须需要有重复实验的能力。
        结果编译：这一阶段显示并汇编了由方法产生的实验。无论观察到的结果是否能被归因于机会而不是一个可观察的效果，统计学意义在这里都是一个重要的概念。
        结论：最后我们要陈述结论，是支持假设还是反对。如果结果并不支持假设，记住方法的弱点对我们依然很重要。相反地，成功的结果也可能是因为不正确的假设。所以，一个方法的所有细节为同行们所知是极其重要的。
      这种研究方法已经用于计算科学研究的多个不同方面。例如，Boehm，Gray和Seewaldt（1984）使用它比较软件工程中的需求说明和原型技术的效用。还 有人将之用以比较搜索和排序算法的效率。信息检索领域的研究者甚至还开发出了带有知名测试数据集的标准方法，并以此评价新搜索引擎的性能。
     在计算科学领域，标准方法面临着很多困难。一个最主要的问题在于，在分析实证测试的结果时许多计算无法以概率描述。例如，许多统计方法需要假设的每次测试都是独立的。这类方法显然无法适用于需要不断优化自身性能的系统，也无法适用于负载均衡等算法。第二，标准实验条件很难适用于计算机科学的产品。例如，我们无法保证一段程序在一类操作环境下的行为与它在另一类操作环境下的相同。这些操作环境甚至可能处于alpha粒子南路内存芯片级别的。第三，从严密控制的实证实验中很难总结结果。例如，仅仅因为一个系统可以在实验条件被用户轻松使用，并不能就得出结论说其它用户在日常工作环境下也能够使用这一系统。最后一点，当足够多的实验支持多个假设时，研究人员很难决策。例如，任何企图证明一个程序总是满足某些性质的尝试终将因为使用标准实验技术而失败。即使是最简单的代码，潜在的程序执行路径的数量也使得测试每条可能执行路径变得不现实。

2.3数学证明

     出于对经验测试技术的不满，许多计算科学的研究者调查了支持具体结论的结构论证的其它方法。英国的研究者侧重于原先用于为人类在哲学领域的论述和思想建模的论证技术。例如，Burrows，Abadi和Needham（1990）采用这种方法为网络论证协议寻找答案。他们工作的核心思想是数学可以用于构建一个包含合法和不合法推论的规则的系统。这些规则可用于在给定一个程序或一些硬件的初始条件下判断一个结论是否合法。
数学推理研究有其自身的发展规则。然而我们可以将两种不同的形式证明方法作为计算科学的研究技术：
     验证——这一方法尝试在一个给定的系统中建立某些好的性质。传统方法允许人们交互地指导理论证明系统使用某些证明序列来得到结论。问题在于即使人们不能构建 一个论点的证明或者证明失败，也不能以此推出这个论点就是不合法。可能存在另一个能够构建出所需的数学论证。
     驳证——这一方法尝试着反驳某一论证，而不是证明某一论证的正确性。通常这一方法会设置预期的系统行为。接着建模检查工具自动地探索预设程序的状态空间，并尝试着找到一个目标结论无法满足的情况。
     数学证明技术非常吸引人。它能为分析计算科学的研究问题提供相似的框架。它还能明确地陈述合法推论的标准以及限制推理过程的范围和适用性的环境条件。然而还有问题挡在数学证明技术成为通用研究工具的道路上。
     第一，数学证明的结果需要令人难以置信的精力去解释。形式证明方法是一个包含论证和可预期的错误的系统。问题就在于在给定的经常使用的数学复杂性质下，错误通常难以检测到。而前面我们提到，实证研究的核心在于你的方法的正确性能被同行开放地审阅。
     第二，形式化证明的范围是有限的。数学的应用在交互和时间先决系统遇到了挑战了。这些问题正在被解决，但还是有很多问题。
     第三的问题与使用形式化技术的代价有关。掌握所需的技巧需要很长一段时间。同样地，它可能需要花费数月为大规模应用证明相对简单的证明。
     最后，形式化证明方法存在的失败还需要更多地讨论。之前我们讨论过，对于实证技术来说，假设证明的失败是有价值的。这很重要。形式化证明的作用通常被非研究者们夸大了。很多这方面的观点都是伪照的。于是，数学推理在应用上的失败应该被视作一种耻辱，而不是同事或同行学习的机会。

2.4解释学

     形式化证明技术依赖于日新月益的数学模型的发展。于是数学模型和它所要呈现的现实之间的关系就带来了许多重要的问题。例如，如果数学模型忽略了程序环境的某些重要方面，那么即使数学证明是安全的，模型实现时也会失败。社会学首先提出了解释学的研究方法。解释学其意为

adj. concerning interpretation, esp. of Scripture or literary texts'.

(牛津简明词典).

     在现实中，这些方法强迫研究者们去观察制品在预期工作环境中的操作和使用。基本前提是抽象模型在现实应用中没有替代品。类似地，可控实验的结果也不能提供通用的，能准确地用于评价那些控制设置之外的性能的结果。特别地，Hawthorne效应认为人和真正的系统在经验设置下的表现非常不同。实验室里的设备的维修和保养是非常不同的。每个人对自己被观察的反应也都是不同的。于是解释学研究依赖于对信号和在工作过程中的观察的解释，而不是直接问人们他们系统的性能。解释学技术敦促人们研究者们进入工作空间。一个极端是，算法的性能只能在现场实验中通过其它应用程序上得到的真实架构下的真实数据集进行评价。这种对最终实现的分析的侧重类似于示例证明。其中的主要区别在于研究者以开放的心态工作，而且没有任何假设需要证明或者反驳（Schman，1987）。由于用户可能以非预期的行为使用程序，定向研究的进行遇到了一些问题。例如，如果当一项或两项搜索结果返回时，用户持续地放弃他们的请求，或者用户只在工作日内使用那些搜索引擎一两次，在这些情况下表明一个搜索引擎快于另一个搜索引擎是很难的。

结论与展望

      计算科学还是一个不成熟的学科。在相对较短的时间里，大量的资源涌入到这个学科里。这给硬件和软件工程都带来了意外的优势。不巧的是，计算技术的发展并没有跟上学术研究技术的发展。在技术目标的追求中，研究者们从其它如哲学、社会学和自然科学————这样不同的学科中借鉴论述和论证的模型。统一的研究框架的缺失是计算科学的现实写照。乐观者可能会认为我们已经从解释学导论学习到很多，并将之应用于需求分析中。类似地，我们还将论证的数学模型导论的知识用于指定和验证复杂系统。然而这篇文章的主要目的在于鼓励人们去思考在我们学科中进行异质性研究所产生的代价。
我不否认计算科学必须要有一个单一的研究框架。然而，我想说的是研究者们必须积极地思考他们所采用的研究传统的长处和弱点。硕士和博士们经常盲目地跟着经验主义或形式证明技术做论文，而不在意那些技术的适用性。例如，传统的解释学得到的结果忽略了商业系统开发的时间和费用限制。形式化方法的研究得到的一些结果已经抽象得远离了问题域，以致无法应用或验证。除非我们开始认识到这些错误，否则我们将继续从其它学科借鉴在计算学科里有缺陷的研究方法的悲剧。

参考文献

• B.W. Boehm, T.E. Gray and T. Seewaldt, Prototyping Vs. Specification: A Multi-Project Experiment, IEEE - Seventh Conference On Software Engineering, 473-484, Computer Society Press, Washington, United States of America, May, 1984.
• M. Burrows, M. Abadi and R. Needham, A Logic of Authentication. ACM Transcations on Computer Systems, 8(1):18-36, 1990.
• N.E. Fuchs, Specifications Are (Preferably) Executable, Software Engineering Journal, 323-334, September 1992.
• A. M. Gravell and P. Henderson, Executing Formal Specifications need not be Harmful, Software Engineering Journal, 104-110, March 1996.
• I.J. Hayes and C.B. Jones (1989), Specifications are not (necessarily) executable, Software Engineering Journal, 1989, 4, (6), pp. 330-338
• C.W. Johnson, Literate Specification, Software Engineering Journal, 225-237, September, 1996.
• L. Suchman, Plans And Situated Actions: The Problem of Human Machine Communication, Cambridge University Press, Cambridge, United Kingdom, 1987.