2

我希望有人可以帮助我解决以下问题，答案将是最好的，但如果你能指出我正确的方向，那也会有所帮助。我是大学最后一年的学生，这些问题来自之前的形式方法考试，我可以知道为今年论文准备的答案。我们的讲师似乎不是最好的，并且没有涵盖很多内容，因此事实证明不可能找到确切的答案。谷歌并没有太大的帮助，也没有推荐的书籍。

1 - 假设 ∃x • P (x) 在逻辑上等价于 ¬∀x • ¬P (x) 并且 ∀x ∈ S • P (x) 意味着 ∀x • x ∈ S ⇒ P (x)，推导出∃x ∈ S • P (x) 表示 ∃x • x ∈ S ∧ P (x)

2 - 描述必须证明的两个陈述以表明定义：

max(i, j)
if i>j
then i
else j

是规范的正确实现：

max(i : Z, j : Z)r : Z
pre true
post (r = i ∨ r = j) ∧ i ≤ r ∧ j ≤ r
4

2 回答 2

2

第一个实际上只是使用给定的和另外两个众所周知的逻辑等价来操作符号：

(1) ∃x • P(x) is logically equivalent to ¬∀x • ¬P(x)
(2) ∀x∈S • P(x) means ∀x • x∈S ⇒ P(x)

∃x∈S • P(x)
== ¬∀x∈S • ¬P(x) (from (1))
== ¬∀x • x∈S ⇒ ¬P(x) (from (2))
== ¬∀x • ¬x∈S v ¬P(x) (from def. of ⇒)
== ¬∀x • ¬(x∈S ∧ P(x)) (from ¬A v ¬B == ¬(A ∧ B))
== ∃x • x∈S ∧ P(x) (from (1) -- the other way around)

对于第二个，您需要认识到 的结果max(i, j)将沿以下两条路径之一计算：一条是何时i<j，另一条是何时i>=j（的逻辑否定i<j）

所以你需要证明

  1. if true ∧ i<j(前置条件), then (r=i ∨ r=j) ∧ i≤r ∧ j≤r(后置条件), and
  2. if true ∧ i>=j(precond.) then (r=i ∨ r=j) ∧ i≤r ∧ j≤r(post cond.),

r结果在哪里max(i, j)

于 2012-05-23T12:40:55.743 回答
1

但是您问题的第 2 节没有意义，因为任何返回 i 或 j 的实现都是正确的。

规范是错误的。

一个正确的后置条件是

post (i > j => r = i) v (i <= j => r = j)
于 2014-08-01T16:33:26.240 回答