Leads-to
program F má vlastnost p ? q iff táto vlastnost môze byt odvodená konecným poctom aplikácií nasledujúcich odvodzovacích pravidiel (tvar hypotéza / záver):
p ensures q / p ? q
p ? q, q ? r / p ? r /* tranzitivita */
??m: m ? W:: p(m) ? q? / ? ?m: m ? W:: p(m) ? q? pre nejakú mnozinu W /* disjunkcia */
Ak p sa stane true, tak q je alebo bude true.
Nemozno však tvrdit, ze p ostane true, az kým q nie je true.
Z „ p leads-to q“ mozno odvodit:
p[Rj] ? ? ?m: m ? j :: q[Rm] ? /* q niekedy platí */
Príklady
1. Z pravidla disjunkcie dostaneme, ze platí nasledovné: p! ? q, p2 ? q / p! ? p2 ? q. Totiz ??m: m ? {1, 2} :: p(m) ? q ? / ? ?m: m ? {1, 2} :: p(m) ? q ?.
2. Pre príklad 2 pre ensures dokázeme, ze
“x ? 0 leads-to x = 0”.
x ? 0 ensures x ? 0 /* z programu */
x ? 0 ? x ? 0 /* z predchádzajúceho */
x ? 0 ensures x = 0 /* z programu */
x ? 0 ? x = 0 /* z predchádzajúceho */
x ? 0 ? x = 0 /* z tranzitivity */