Theorems about ensures

• Reflexívnost:

  p ensures p
  

Dôkaz: p unless p a ?S platí {p ? ?p} S {p}. Kedze kazdý program obsahuje aspon jeden príkaz, tvrdenie je dokázané.

• Zoslabenie:

  p ensures q, q ? r / p ensures r
  

Dôkaz:

• zoslabenie pre unless platí, stací teda ukázat, ze ak ?S také, ze {p ? ?q} S {q}, potom {p ? ?r} S {r}
• Vyplýva to z q ? r, ?r ? ?q a teda
  p ? ?r ? p ? ?q

• Nemoznost:

  p ensures false / ?p
  

Dôkaz: z “p ensures false” vieme, ze ?S {p} S {false}

teda p ? false

• Konjunkcia

  p ensures q, p’ ensures q’ /
  
  / (p ? p’) ensures (p ? q’) ? (p’ ? q) ? (q ? q’)

Dôkaz: podobný ako pre unless

• Disjukcia

  p ensures q / p ? r ensures q ? r
  

Dôkaz: z definície

Previous slide

Next slide

Back to first slide

View graphic version