Ensures

• (daný je program F)

• p ensures q ? p unless q ? ??S: S in F :: {p ? ?q} S {q}?

• Ak p je true v nejakom bode výpoctu, p ostane true, pokial q je false (p unless q) a urcite raz (eventually) sa stane q true („raz nan dôjde“)

• Z „ p ensures q“ mozno odvodit: p[Rj] ?

  ? ?m: m ? j :: q[Rm] ? ? /* q niekedy platí */
  
  ? ?k: j ? k < m :: (p ? ?q)[Rk] ? /* dovtedy platí p ??q */

• Príklady

  1. x je neklesajúca a raz stúpne
  
  • x = k ensures x > k, teda
  • ? ?k :: x = k unless x > k ?,
  • ? ?k :: ? ?S :: {x = k} S {x > k} ??
  2. Program x := 0 if x < 0  x := 0 if x > 0
  • “x ? 0 ensures x = 0” nie je vlastnost tohto programu, lebo neexistuje S také, ze {x ? 0} S {x = 0}, pretoze ak je to prvá cast (teda x := 0 if x < 0), potom
    {x ? 0} x := 0 if x < 0 {x = 0}
    
    {x ? 0 ? x < 0} x := 0 {x = 0}
  • hladáme taký vstup, ze táto podmienka NEPLATÍ:
    {x ? 0 ? ?(x < 0)} empty {x = 0}
    
  • totiz priradenie x := 0 sa nevykoná (príkaz empty) pre x > 0 a potom výstupná podmienka x = 0 nebude platit
  • rovnako nemôze vyhovovat ani druhá cast

Previous slide

Next slide

Back to first slide

View graphic version