proof - 我需要一个函数后置条件的证明

Question

这是一项家庭作业，但我无法通过编写正式的证明来了解整个业务。任何人都可以破解这个并为这个 fnc 的后置条件写正式证明：

字符串 REPLACE_BY (字符串 s,char c,char d)

后置条件 返回值是由 s 形成的字符串，通过将每次出现的 c 替换为 d（否则保持 s 不变）。

Answer 1

为了证明函数的正确性（即，如果输入符合给定的前置条件，则符合后置条件），您需要函数的实现。

我将通过给你需要工作的假设来帮助你开始，但因为这是家庭作业，所以将证明留给你。

假设是：

1. 该方法定义如下：

   String replace_by(String s, char c, char d) {
       for (int i = 0; i < s.size();++i) { 
           if (s[i] == c) {
               s[i] = d;
           }
       } 
       return s;
   }
   

2. 前提是s != null /\ s.size() < Integer.MAX_VALUE

3. old(s)用于引用s进入函数前的值

4. 散文中给出的后置条件的正式规范是

   old(s) != null /\ s != null /\
   \-/i in 0..(old(s).size()-1): (
          ((old(s)[i] == old(c)) && (s[i] == old(d)))
       \/ ((old(s)[i] != old(c)) && (s[i] == old(s)[i]))
   )
   /\ old(s).size() == s.size()
   

   （\-/是逻辑 for-all 运算符，\/是 'or' 和/\是 'and'）

有了这个，你应该能够建立一个基于Hoare 逻辑的证明。