Доказательство правильности в формальной логике

Question

Мне было интересно, если кто-нибудь может помочь мне ответить на этот вопрос. Это из предыдущей экзаменационной работы, и я смог узнать ответ, готовый к экзамену этого года.

Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно он просит?

Рассмотрим следующий раздел кода с целочисленными переменными:

if (i < j) {
    m = i;
} else {
    m = j;
}

Указав соответствующее условие вывода и проверив правильность фрагмента кода, докажите, что после выполнения m равно минимуму i и j.

У меня есть пост сообщение как: {m = i ∧ i

это правильно? и как ты это проверяешь? Вроде все просто.

Благодарю.

Answer 1

Ваше сообщение правильно Я лично считаю следующий вариант (который эквивалентен) более естественным, хотя:

(i<j → m=i) ∧ (i≥j → m=j)

Чтобы доказать, что программа удовлетворяет условию post, выполните следующие действия.

1. Обратите внимание, что для того, чтобы программа всегда удовлетворяла условию публикации, вы должны использовать true как ваше предварительное условие.

2. Итак, у вас есть следующая тройка Хоара:

   {true}
   if (i < j) {
   
   
       m = i;
   
   } else {
   
   
       m = j;
   
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

3. Постусловие должно сохраняться в конце обеих ветвей, поэтому (согласно стандартному самому слабому правилу предварительных условий для условных выражений) мы имеем

   {true}
   if (i < j) {
   
   
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--.
   } else {                                       |
                                                  |
                                                  |
       m = j;                                     |   copy
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--|
   }                                              |
   {(i < j → m = i) ∧ (i ≥ j → m = j)}  ----------'
   

4. Продвигая формулу вверх в соответствии с самой слабой предпосылкой для уступки доходности

   {true}
   if (i < j) {
   
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   <---.
       m = i;                                    | m replaced by i
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   } else {
   
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   <---.
       m = j;                                    | m replaced by j
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

5. На вершине истинной ветви мы знаем, что i < jи в верхней части ветки else мы знаем, что ¬(i < j):

   {true}
   if (i < j) {
       {i < j}                               (1)  <--- added
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   (2)
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   } else {
       {¬(i < j)}                            (3)  <--- added
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   (4)
       m = j;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

6. Осталось показать для любых двух последовательных утверждений, первое утверждение подразумевает второе. (Они обычно называются "доказательствами обязательств".) У нас есть два таких обязательства: (1) должно подразумевать (2) а также (3) должно подразумевать (4), Это явно так.

   - "Кед":-)