proof - 関数事後条件の証明が必要です

Question

これは宿題ですが、正式な証明を書くことでこのビジネス全体を理解することはできません。誰かがこれを解読して、この fnc の事後条件の正式な証明を書くことができますか?

文字列 REPLACE_BY (文字列 s、文字 c、文字 d)

事後条件 返される値は、出現するすべての c を d で置き換えることによって s から形成された文字列です (それ以外の場合は 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()
   

   (\-/はすべての論理演算子で、\/「or」および/\「and」です)

これで、 Hoare 論理に基づいた証明を構築できるはずです。