当前位置：文江博客话题详情

我需要函数后置条件的证明

发布于 2024-10-22 22:12:20 字数 192 浏览 0 评论 0原文

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

string REPLACE_BY (string s,char c,char d)

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

冷…雨湿花 2024-10-29 22:12:21

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

我将首先向您提供工作所需的假设，但将证明留给您，因为这是家庭作业。

假设是：

该方法定义如下：

字符串replace_by(字符串s, 字符c, 字符d) {
    for (int i = 0; i < s.size();++i) { 
        如果 (s[i] == c) {
            s[i] = d；
        }
    } 
    返回 s；
}

前提条件是 s != null /\ s.size() < Integer.MAX_VALUE
old(s) 用于引用进入函数之前s的值

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

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

（\-/ 是逻辑 for-all 运算符，\/ 是“或”，/\ 是“与”）

有了这个，您应该能够基于构建证明霍尔逻辑。

In order to proove the correctness of the function (i.e. compliance to a post-condition if the input conforms to a given pre-condition), you need the function's implementation.

I will get you started by giving you the assumptions under which you will need to work, but leave the proof up to you since it's homework.

The assumptions are:

that the method is defined as such:

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;
}

that the precondition is s != null /\ s.size() < Integer.MAX_VALUE
old(s) is used to refer to the value of s before entering the function

that the formal specification of your postcondition given in prose is

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()

(\-/ is the logical for-all operator, \/ is 'or' and /\ is 'and')

With this, you should be able to build a proof based on Hoare logic.

回复收藏 0 原文

~没有更多了~