你如何证明一个函数有效? [英] How do you prove a function works?

问题描述

我最近开始热衷于测试，并且主要从单元测试开始.我编写单元测试来说明函数在某些情况下工作，特别是使用我正在使用的确切输入.我可能会做一些单元测试来锻炼这个功能.尽管如此，除了该函数在我测试过的场景下完成了我期望它做的事情之外，我实际上还没有证明任何其他事情.可能还有其他我没有想到的输入和场景，并且考虑边缘情况是昂贵的，尤其是在边缘情况下.

I've recently gotten the testing religion and have started primarily with unit testing. I code unit tests which illustrate that a function works under certain cases, specifically using the exact inputs I'm using. I may do a number of unit tests to exercise the function. Still, I haven't actually proved anything other than the function does what I expect it to do under the scenarios I've tested. There may be other inputs and scenarios I haven't thought of and thinking of edge cases is expensive, particularly on the margins.

这一切对我来说都不是很令人满意.当我开始考虑必须提出测试以满足分支和路径覆盖率，然后进行集成测试时，预期的排列可能会变得有点令人抓狂.

This is all not very satisfying to do me. When I start to think of having to come up with tests to satisfy branch and path coverage and then integration testing, the prospective permutations can become a little maddening.

所以，我的问题是，如何证明(与证明数学中的定理一样)函数有效(并且，在完美世界中，将这些证明"组合成系统有效的证明)?

So, my question is, how can one prove (in the same vein of proving a theorem in mathematics) that a function works (and, in a perfect world, compose these 'proofs' into a proof that a system works)?

是否有某个测试领域涵盖了一种方法，您试图通过证明系统的所有功能正常工作来证明系统正常工作?学术界以外的人是否会打扰这样的方法?是否有工具和技术可以提供帮助?

Is there a certain area of testing that covers an approach where you seek to prove a system works by proving that all of its functions work? Does anybody outside of academia bother with an approach like this? Are there tools and techniques to help?

我意识到我对工作"这个词的使用并不准确.我想我的意思是当一个函数执行某些规范(书面或暗示)规定它应该执行的操作并且除此之外什么都不做时，它才能工作.

I realize that my use of the word 'work' is not precise. I guess I mean that a function works when it does what some spec (written or implied) states that it should do and does nothing other than that.

注意，我不是数学家，只是程序员.

Note, I'm not a mathematician, just a programmer.

推荐答案

在学术界，有一个类似于数学归纳法的概念，叫做结构归纳法.但是，它仅适用于完全没有副作用的函数式编程语言和方法.在其他情况下，由于副作用，很难(如果不是不可能的话)证明一种方法有效.

In academica, there is a concept similar to induction in mathematics, it's called structural induction. However, it only applies to functional programming languages and methods with no side effects at all. In others, it is very hard, if not impossible, to prove that a method works due to side effects.

在 TDD 中，您尝试制定方法必须满足的边缘情况才能有效，但是，可能会遗漏这种情况.即使(非平凡的)方法满足您的所有测试，也可能存在您根本没有想到的参数组合或一系列事件会破坏您的代码.简单地说:这就是生活.您可以在一个非平凡的实现中预测所有结果，但您可以确保该方法适用于特定的边缘情况，预计某些情况非常前卫，您会在接触它们时割伤自己.(zing，糟糕的双关语).

In TDD, you try to formulate edge cases which a method has to fulfill to be valid, however, it is possible to miss such a case. Even if a (non-trivial) method fulfills all your tests, there can be a combination of arguments or a sequence of events you simply didn't think of which will break your code. Simply put: That's life. You can possibly predict all outcomes in a non-trivial implementation, but you can assure that the method works for specific edge cases, expect for some cases that are so edgy you will cut yourself upon touching them. (zing, bad pun).

这篇关于你如何证明一个函数有效?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！