Theorems about ensures 2

• Dôsledok 1.

  p ? q / p ensures q
  

Dôkaz: p unless q a zoslabenie

• Dôsledok 2. („Prešmyk“)

  p ? q ensures r / p ensures q ? r
  

Dôkaz:

p ? q unless r /* z predpokladu */

p unless q ? r /* dôsledok 4 pre unless */
p ? q ensures r /* predpoklad */
p ensures q ? r /* konjunkcia a zoslabenie */

• Dôsledok 3.

  p unless q ? r / p ? ?q unless q ? r
  

Dôkaz:

p ensures q ? r /* predpoklad */

(p ? q) ? (p ? ?q) ensures q ? r
p ? ?q ensures (p ? q) ? q ? r /* z dôsledku 2 */
p ? ?q ensures q ? r

Previous slide

Next slide

Back to first slide

View graphic version