TL;DR：我如何证明算法适用于每个 n 值？
概述：
我是一名自学成才的程序员，具有线性代数的数学背景。我最近需要通过编写一个算法来解决 n=100 的问题来证明关系是递归的。
当我找到解决方案时，我到达那里的方式被认为是不可接受的。与我交谈的人说我的算法是一种“统计”算法，而不是实际证明存在递归关系并证明我的算法可以工作。
我一直在解决诸如 codesignal、hackerrank 等网站上的一些问题，但这是我第一次遇到这种将解决方案推广到正式证明的概念。
问题：如何证明算法适用于每个 n 值？
示例：让我们以二进制搜索为例，忘记我遇到的实际问题。
如果您有一个由 100 个整数组成的数组，按升序排序，您如何证明您的二进制搜索算法适用于任何数组和任何 n？
在下面的示例中，假设我们的数组是
arr = list(range(100))
我提出的问题是：
编写一个递归算法，如果值 '42' 在数组中，则返回 True，否则返回 False。
你如何证明（如正式证明）这个算法有效？请注意强调算法从启发式解决方案转变为证明算法的那一刻背后的思维过程和直觉？
如果一个数组A是排序的，那么如果我们可以证明A[x] > 42，那么A[x + 1] > 42。这是因为，如果对数组进行排序，则每个元素都大于或等于其前身（即A[x + 1] > A[x] > 42）。我们知道这一点是因为>运算符是传递的。
反过来，对于<操作员也是如此。
二进制搜索应在每一步中拒绝所有大于或小于所需输入的输入，方法是对单个可能性进行采样，并确定其一侧的所有输入也需要拒绝（如上所述）。
（编辑：如果x > 42或x < 42为真；那么x = 42必须为假。）
在每个步骤中，至少删除数组的一个元素，除非它等于 42。这是因为如果元素不是 42，那么该元素（可能与其他元素一起）将被删除。
如果数组越来越小（假设没有采样 42），并且永远不会删除 42，那么在某些时候，要么采样 42，要么数组为空
如果数组为空，并且由于没有丢弃 42，则永远不会有 42。
如果我们对 42 进行采样，因为没有向数组中引入新元素，所以从 42 开始。
证明！
为了证明递归算法有效，你想证明它
它结束是因为在每个递归步骤中，数组变得越来越小（但不能低于 []）。它产生了正确的结果，因为 42 从未被删除或添加——所以最后，如果我们找不到 42，那是因为它从未存在过。在我看来，你的论点不应该依赖任何具体的例子，除了基本情况——否则它可能是统计的。您需要在数学意义上“证明”它。
对于一个简单的正确性证明：您需要证明您的算法可以成功地完成它的设计目标。
因此，以关于输入案例数据的语句为前提。并计算出它应该暗示输出中所需的后置条件。这证明算法是正确的。
P：关于给定输入的声明
问：所需输出的声明。
证明 P 蕴含 Q。
照顾角落的情况。确保在所有情况下终止算法。如果它是递归算法，则您严格需要证明算法终止/退出。
编写一个递归算法，如果值 '42' 在数组中，则返回 True，否则返回 False。
对于此类问题，您还可以使用Proof by contrast。首先尝试假设如果 42 不存在该算法将返回 true，或者如果 42 存在该算法将返回 false。然后，通过你的算法流程证明你的假设是正确的，并试图证明这是不可能的，一个矛盾的。