我需要一个函数后置条件的证明
这是一个家庭作业，但我无法通过撰写正式的证据来了解整个业务。任何人都可以破解这个并为此fnc的后置条件写正式证明：
string REPLACE_BY（string s，char c，char d）
postcondition返回值是通过替换每个匹配项从s形成的字符串
c由d表示（否则保持不变）。
没有找到相关结果
已邀请:
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; }用于在进入功能之前参考的值 散文中给出的后置条件的正式规范是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运算符，是'或'，而是'和'） 有了这个，您应该能够基于Hoare逻辑构建证明。