I need a proof for a function postcondition

Question

this is a homework but I just cannot get my head around this whole business with writing formal prooves. Could anyone crack this and write formal proof for postcondition of this fnc:

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

postcondition The returned value is the string formed from s by replacing every occurrence of c by d (and otherwise leaving s unchanged).

maybe.. this belongs on cstheory.stackexchange.com? not sure? — gideon
@giddy: Nope. Cstheory is for research-level questions only. — sepp2k
Shouldn't every professional programmer be able to do such things? Isn't that part of a being programmer? — There is nothing we can do
I know you're having trouble wrapping your head around this prove business and all, but as a general rule when trying to prove that a function meets a given post-condition, you start by looking at the function's definition... which you did not include in the question. — sepp2k
@sepp2k isn't fnc declaration and "worded" postcondition sufficient for this task (I wasn't given definition at all by the way)? What for would one need to see guts of a fnc in order to be able to give formal proof for postcondition? — There is nothing we can do

blubb blubb · Accepted Answer · 2011-03-29T19:23:26

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.

I need a proof for a function postcondition

1 Answers