I need a proof for a function postcondition

this is a homework but I just cannot get my head around this whole business with writing formal prooves. Could an开发者_JAVA技巧yone 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).

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:

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

2. that the precondition is s != null /\ s.size() < Integer.MAX_VALUE

3. old(s) is used to refer to the value of s before entering the function

4. 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.