Мне нужно доказательство для постусловия функции

Question

это домашнее задание, но я просто не могу разобраться в этом бизнесе с написанием формальных доказательств.Может ли кто-нибудь взломать это и написать формальное доказательство для постусловия этого fnc:

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

postcondition Возвращаемое значение являетсястрока, сформированная из s, заменяя каждое вхождение c на d (и оставляя 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()
   

   (\-/ является логическимдля всех, \/ is 'or' и /\ is 'and')

С этим вы сможете создать доказательство на основе Hoareлогика .