问题标签 [proofs]

假设我可以访问 https 天气 API。假设我在 2017 年 8 月 17 日星期四 23:30 查询了它的健康状态，API 回复 OK（简单的 OK http 代码）。

作为客户，我需要在未来证明该服务确实响应了我这些数据。

我正在考虑要求 API 添加已发送数据的加密签名 + 时间戳，以证明他们在该特定时间确实响应正常。是不是矫枉过正？有没有更简单的方法呢？

我很难理解为什么下面的每个示例都有效或无效，更抽象地说，归纳如何与战术与 Isar 相互作用。我正在使用最新的 Isabelle/HOL（2016-1）在 Windows 10 上的 Isabelle/HOL（2016 年 12 月）编程和证明 4.3

有 8 种情况：引理是长的（包括明确的名称）或短的、结构化的（使用assumesand shows）或非结构化的（使用箭头），证明是结构化的（Isar）或非结构化的（战术性的）。

1. 结构化短引理和结构化证明

2. 非结构化短引理和结构化证明

3. 结构化长引理和结构化证明

4. 非结构化长引理和结构化证明

**5。结构化短引理和非结构化证明*

6. 非结构化短引理和非结构化证明

7. 结构化长引理和非结构化证明

8. 非结构化长引理和非结构化证明

我将如何继续证明这两个函数的类型正确？我对这个问题有点迷茫。

我试图证明“前置”的前提条件在执行下面的程序期间成立。前提是：

我在下面的代码中以 pragma 的形式尝试证明这一点。我可以证明这个前提条件适用于单循环，但不适用于双循环。尽管我找到了非常复杂的循环不变量的示例，但我找不到任何双循环示例。

规格：

身体：

错误是“循环不变量可能在第一次迭代中失败，无法证明 Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y” 它并没有说它可能在第一次迭代后失败，所以这就是问题。

我试图证明下面给出的最大子数组问题的蛮力版本的正确性：

但我似乎被困在设计循环不变量上，这可能是因为内部循环改变了一个全局变量（max），这使得我很难描述（max）在对应于内部循环的循环不变量中代表什么。

我的尝试：

总体而言，该算法通过查找以下子数组的最大子数组来工作：

• 内循环不变量：
  • Current_sum 是数组 [i...j] 中所有元素的总和
  • 卡在这里，因为我似乎无法捕捉到 i 和 j 的最大值，因此左和右

我正在比较Nats和Lists的关联性证明。

Lists 上的证明是通过归纳法进行的

但是，关于 Nats 的证明是

为什么我不需要对nat_add_assoc证明进行归纳？是因为自然数上发生了一些自动化吗？